1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Chris Hughes
5 -/
6
7 import data.int.modeq data.int.gcd data.fintype data.pnat.basic tactic.ring
src └────────────┘ └──────────┘ └──────────┘ └─────────────┘ └─────────┘
8
9 /-!
10 # Integers mod `n`
11
12 Definition of the integers mod n, and the field structure on the integers mod p.
13
14 There are two types defined, `zmod n`, which is for integers modulo a positive nat `n : ℕ+`.
15 `zmodp` is the type of integers modulo a prime number, for which a field structure is defined.
16
17 ## Definitions
18
19 * `val` is inherited from `fin` and returns the least natural number in the equivalence class
20
21 * `val_min_abs` returns the integer closest to zero in the equivalence class.
22
23 * A coercion `cast` is defined from `zmod n` into any semiring. This is a semiring hom if the ring has
24 characteristic dividing `n`
25
26 ## Implentation notes
27
28 `zmod` and `zmodp` are implemented as different types so that the field instance for `zmodp` can be
29 synthesized. This leads to a lot of code duplication and most of the functions and theorems for
30 `zmod` are restated for `zmodp`
31 -/
32
33 open nat nat.modeq int
34
35 def zmod (n : ℕ+) := fin n
id └┘ └─┘ ┴
src └┘ └─┘
typ └┘ └─┘ ┴
doc └┘
36
37 namespace zmod
38
39 instance (n : ℕ+) : has_neg (zmod n) :=
id └┘ └─────┘ └──┘ ┴
src └┘ └─────┘ └──┘
typ └┘ └─────┘ └──┘ ┴
doc └┘
40 ⟨λ a, ⟨nat_mod (-(a.1 : ℤ)) n,
id ┴ └─────┘ ┴ ┴┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ ┴ └─────┘ ┴ ┴┴ ┴ ┴
41 have h : (n : ℤ) ≠ 0 := int.coe_nat_ne_zero_iff_pos.2 n.pos,
id ┴ ┴ ┴ └─────────────────────────┘┴ ┴└──┘
src ┴ ┴ └─────────────────────────┘┴ └──┘
typ ┴ ┴ ┴ └─────────────────────────┘┴ ┴└──┘
42 have h₁ : ((n : ℕ) : ℤ) = abs n := (abs_of_nonneg (int.coe_nat_nonneg n)).symm,
id ┴ ┴ ┴ ┴ └─┘ ┴ └───────────┘ └────────────────┘ ┴ └──┘
src ┴ ┴ ┴ └─┘ └───────────┘ └────────────────┘ └──┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ └───────────┘ └────────────────┘ ┴ └──┘
43 by rw [← int.coe_nat_lt, nat_mod, to_nat_of_nonneg (int.mod_nonneg _ h), h₁];
id └────────────┘ └─────┘ └──────────────┘ └────────────┘ ┴ └┘
src └────┘└────────────┘└┘└─────┘└┘└──────────────┘┴ └────────────┘└─┘ └─┘ ┴
typ └────┘└────────────┘└┘└─────┘└┘└──────────────┘┴ └────────────┘└─┘┴└─┘└┘┴
doc └────┘ └┘ └┘ ┴ └─┘ └─┘ ┴
txt └────┘ └┘ └┘ ┴ └─┘ └─┘ ┴
par └────┘ └┘ └┘ ┴ └─┘ └─┘ ┴
pid └──┘ └┘ └┘ ┴ └─┘ └─┘ ┴
st └───────────────────┘└───────┘└─────────────────────────────────────┘└──┘┴└─
44 exact int.mod_lt _ h⟩⟩
id └────────┘ ┴
src └────┘└────────┘└─┘
typ └────┘└────────┘└─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───────────────────────┘
45
46 instance (n : ℕ+) : add_comm_semigroup (zmod n) :=
id └┘ └────────────────┘ └──┘ ┴
src └┘ └────────────────┘ └──┘
typ └┘ └────────────────┘ └──┘ ┴
doc └┘
47 { add_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id ┴┴ ┴┴ ┴┴ └───────────┘
src └───────────┘
typ ┴┴ ┴┴ ┴┴ └───────────┘
48 (show ((a + b) % n + c) ≡ (a + (b + c) % n) [MOD n],
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
doc ┴ └──┘ ┴
49 from calc ((a + b) % n + c) ≡ a + b + c [MOD n] : modeq_add (nat.mod_mod _ _) rfl
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
src ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
50 ... ≡ a + (b + c) [MOD n] : by rw add_assoc
id ┴ ┴ └───────┘
src ┴ ┴ └─┘└───────┘└
typ ┴ ┴ └─┘└───────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └─────────────
51 ... ≡ (a + (b + c) % n) [MOD n] : modeq_add rfl (nat.mod_mod _ _).symm),
id ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
src ─────┘ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
typ ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘
52 add_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a + b) % n = (b + a) % n, by rw add_comm),
id ┴┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘
typ ┴┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └──────────┘
53 ..fin.has_add }
id └─────────┘
src └─────────┘
typ └─────────┘
54
55 instance (n : ℕ+) : comm_semigroup (zmod n) :=
id └┘ └────────────┘ └──┘ ┴
src └┘ └────────────┘ └──┘
typ └┘ └────────────┘ └──┘ ┴
doc └┘
56 { mul_assoc := λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id ┴┴ ┴┴ ┴┴ └───────────┘
src └───────────┘
typ ┴┴ ┴┴ ┴┴ └───────────┘
57 (calc ((a * b) % n * c) ≡ a * b * c [MOD n] : modeq_mul (nat.mod_mod _ _) rfl
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
src ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └─┘
58 ... ≡ a * (b * c) [MOD n] : by rw mul_assoc
id ┴ ┴ └───────┘
src ┴ ┴ └─┘└───────┘└
typ ┴ ┴ └─┘└───────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └─────────────
59 ... ≡ a * (b * c % n) [MOD n] : modeq_mul rfl (nat.mod_mod _ _).symm),
id ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
src ─────┘ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
typ ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘ └──┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘
60 mul_comm := λ ⟨a, _⟩ ⟨b, _⟩, fin.eq_of_veq (show (a * b) % n = (b * a) % n, by rw mul_comm),
id ┴┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘
typ ┴┴ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └──────────┘
61 ..fin.has_mul }
id └─────────┘
src └─────────┘
typ └─────────┘
62
63 instance (n : ℕ+) : has_one (zmod n) := ⟨⟨(1 % n), nat.mod_lt _ n.pos⟩⟩
id └┘ └─────┘ └──┘ ┴ ┴ ┴ └────────┘ ┴└──┘
src └┘ └─────┘ └──┘ ┴ └────────┘ └──┘
typ └┘ └─────┘ └──┘ ┴ ┴ ┴ └────────┘ ┴└──┘
doc └┘
64
65 instance (n : ℕ+) : has_zero (zmod n) := ⟨⟨0, n.pos⟩⟩
id └┘ └──────┘ └──┘ ┴ ┴└──┘
src └┘ └──────┘ └──┘ └──┘
typ └┘ └──────┘ └──┘ ┴ ┴└──┘
doc └┘
66
67 instance (n : ℕ+) : inhabited (zmod n) := ⟨0⟩
id └┘ └───────┘ └──┘ ┴
src └┘ └───────┘ └──┘
typ └┘ └───────┘ └──┘ ┴
doc └┘
68
69 instance zmod_one.subsingleton : subsingleton (zmod 1) :=
id └──────────┘ └──┘
src └──────────┘ └──┘
typ └──────────┘ └──┘
70 ⟨λ a b, fin.eq_of_veq (by rw [eq_zero_of_le_zero (le_of_lt_succ a.2),
id ┴ ┴ └───────────┘ └────────────────┘ └───────────┘ ┴
src └───────────┘ └──┘└────────────────┘┴ └───────────┘┴ └────
typ ┴ ┴ └───────────┘ └──┘└────────────────┘┴ └───────────┘┴┴└────
doc └──┘ ┴ ┴ └────
txt └──┘ ┴ ┴ └────
par └──┘ ┴ ┴ └────
pid └┘ ┴ ┴ └────
st └─────────────────────────────────────────┘└─
71 eq_zero_of_le_zero (le_of_lt_succ b.2)])⟩
id └────────────────┘ └───────────┘ ┴
src ─┘└────────────────┘┴ └───────────┘┴ └──┘
typ ─┘└────────────────┘┴ └───────────┘┴┴└──┘
doc ─┘ ┴ ┴ └──┘
txt ─┘ ┴ ┴ └──┘
par ─┘ ┴ ┴ └──┘
pid ─┘ ┴ ┴ └──┘
st ───────────────────────────────────────┘┴
72
73 lemma add_val {n : ℕ+} : ∀ a b : zmod n, (a + b).val = (a.val + b.val) % n
id └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
src └┘ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴
typ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
doc └┘
74 | ⟨_, _⟩ ⟨_, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
75
76 lemma mul_val {n : ℕ+} : ∀ a b : zmod n, (a * b).val = (a.val * b.val) % n
id └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
src └┘ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴
typ └┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
doc └┘
77 | ⟨_, _⟩ ⟨_, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
78
79 lemma one_val {n : ℕ+} : (1 : zmod n).val = 1 % n := rfl
id └┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └─┘
src └┘ └──┘ └─┘ ┴ ┴ └─┘
typ └┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └─┘
doc └┘
80
81 @[simp] lemma zero_val (n : ℕ+) : (0 : zmod n).val = 0 := rfl
id └┘ └──┘ ┴ └─┘ ┴ └─┘
src └┘ └──┘ └─┘ ┴ └─┘
typ └┘ └──┘ ┴ └─┘ ┴ └─┘
doc └──┘ └┘
82
83 private lemma one_mul_aux (n : ℕ+) (a : zmod n) : (1 : zmod n) * a = a :=
id └┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ ┴ ┴
typ └┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └┘
84 begin
st └─────
85 cases n with n hn,
id ┴
src └────┘ └────────┘
typ └────┘┴└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ──────────────────┘└─
86 cases n with n,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ───────────────┘└─
87 { exact (lt_irrefl _ hn).elim },
id └───────┘ └┘
src └────┘ └───────┘└─┘ └─────┘
typ └────┘ └───────┘└─┘└┘└─────┘
doc └────┘ └─┘ └─────┘
txt └────┘ └─┘ └─────┘
par └────┘ └─┘ └─────┘
pid ┴ └─┘ └───┘└┘
st ───┘└──────────────────────────┘└┘└
88 { cases n with n,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
89 { exact @subsingleton.elim (zmod 1) _ _ _ },
id └───────────────┘ └──┘
src └────┘ └───────────────┘┴ └──┘└────────┘
typ └────┘ └───────────────┘┴ └──┘└────────┘
doc └────┘ ┴ └────────┘
txt └────┘ ┴ └────────┘
par └────┘ ┴ └────────┘
pid ┴ ┴ └───────┘┴
st ─────┘└──────────────────────────────────────┘└┘└
90 { have h₁ : a.1 % n.succ.succ = a.1 := nat.mod_eq_of_lt a.2,
id ┴ └─────────┘ ┴ ┴ └──────────────┘ ┴
src └────────┘ └─┘┴┴└─────────┘┴┴┴ └────┘└──────────────┘┴ └┘
typ └────────┘ └─┘┴┴└─────────┘┴┴┴┴└────┘└──────────────┘┴┴└┘
doc └────────┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └┘
txt └────────┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └┘
par └────────┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └┘
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ └────┘ ┴ └┘
st ──────────────────────────────────────────────────────────────┘└─
91 have h₂ : 1 % n.succ.succ = 1 := nat.mod_eq_of_lt dec_trivial,
id └─────────┘ └──────────────┘ └─────────┘
src └──────────┘ ┴└─────────┘┴ └────┘└──────────────┘┴└─────────┘
typ └──────────┘ ┴└─────────┘┴ └────┘└──────────────┘┴└─────────┘
doc └──────────┘ ┴ ┴ └────┘ ┴└─────────┘
txt └──────────┘ ┴ ┴ └────┘ ┴
par └──────────┘ ┴ ┴ └────┘ ┴
pid └─────┘└───┘ ┴ ┴ ┴└───┘ ┴
st ──────────────────────────────────────────────────────────────────┘└─
92 refine fin.eq_of_veq _,
id └───────────┘
src └─────┘└───────────┘└┘
typ └─────┘└───────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ───────────────────────────┘└─
93 simp [mul_val, one_val, h₁, h₂] } }
id └─────┘ └─────┘ └┘ └┘
src └────┘└─────┘└┘└─────┘└┘ └┘ └┘
typ └────┘└─────┘└┘└─────┘└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────┘└───
94 end
st ──┘
95
96 private lemma left_distrib_aux (n : ℕ+) : ∀ a b c : zmod n, a * (b + c) = a * b + a * c :=
id └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
97 λ ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, fin.eq_of_veq
id ┴┴ ┴┴ ┴┴ └───────────┘
src └───────────┘
typ ┴┴ ┴┴ ┴┴ └───────────┘
98 (calc a * ((b + c) % n) ≡ a * (b + c) [MOD n] : modeq_mul rfl (nat.mod_mod _ _)
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘
src ┴ ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─┘ └─────────┘
99 ... ≡ a * b + a * c [MOD n] : by rw mul_add
id ┴ ┴ ┴ └─────┘
src ┴ ┴ ┴ └─┘└─────┘└
typ ┴ ┴ ┴ └─┘└─────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └───────────
100 ... ≡ (a * b) % n + (a * c) % n [MOD n] : modeq_add (nat.mod_mod _ _).symm (nat.mod_mod _ _).symm)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └──┘ └─────────┘ └──┘
src ─┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └──┘ └─────────┘ └──┘
typ ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ └──┘ └─────────┘ └──┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
101
102 instance (n : ℕ+) : comm_ring (zmod n) :=
id └┘ └───────┘ └──┘ ┴
src └┘ └───────┘ └──┘
typ └┘ └───────┘ └──┘ ┴
doc └┘
103 { zero_add := λ ⟨a, ha⟩, fin.eq_of_veq (show (0 + a) % n = a, by rw zero_add; exact nat.mod_eq_of_lt ha),
id ┴┴ └───────────┘ ┴ ┴ ┴ ┴ └──────┘ └──────────────┘ └┘
src └───────────┘ ┴ ┴ ┴ └─┘└──────┘ └────┘└──────────────┘┴
typ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ └─┘└──────┘ └────┘└──────────────┘┴└┘
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────────────────────────────────┘
104 add_zero := λ ⟨a, ha⟩, fin.eq_of_veq (nat.mod_eq_of_lt ha),
id ┴ └┘ └───────────┘ └──────────────┘
src └───────────┘ └──────────────┘
typ ┴ └┘ └───────────┘ └──────────────┘
105 add_left_neg :=
106 λ ⟨a, ha⟩, fin.eq_of_veq (show (((-a : ℤ) % n).to_nat + a) % n = 0,
id ┴┴ └───────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
typ ┴┴ └───────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
107 from int.coe_nat_inj
id └─────────────┘
src └─────────────┘
typ └─────────────┘
108 begin
st └─────
109 have hn : (n : ℤ) ≠ 0 := (ne_of_lt (int.coe_nat_lt.2 n.pos)).symm,
id ┴ ┴ ┴ └──────┘ └────────────┘ └───┘
src └────────┘ └─┘┴└┘┴└────┘ └──────┘┴ └────────────┘└─┘└───┘└─────┘
typ └────────┘ ┴└─┘┴└┘┴└────┘ └──────┘┴ └────────────┘└─┘└───┘└─────┘
doc └────────┘ └─┘ └┘ └────┘ ┴ └─┘ └─────┘
txt └────────┘ └─┘ └┘ └────┘ ┴ └─┘ └─────┘
par └────────┘ └─┘ └┘ └────┘ ┴ └─┘ └─────┘
pid └─────┘└─┘ └─┘ └┘ ┴└───┘ ┴ └─┘ └────┘┴
st ────────────────────────────────────────────────────────────────────────┘└─
110 rw [int.coe_nat_mod, int.coe_nat_add, to_nat_of_nonneg (int.mod_nonneg _ hn), add_comm],
id └─────────────┘ └─────────────┘ └──────────────┘ └────────────┘ └┘ └──────┘
src └──┘└─────────────┘└┘└─────────────┘└┘└──────────────┘┴ └────────────┘└─┘ └─┘└──────┘┴
typ └──┘└─────────────┘└┘└─────────────┘└┘└──────────────┘┴ └────────────┘└─┘└┘└─┘└──────┘┴
doc └──┘ └┘ └┘ ┴ └─┘ └─┘ ┴
txt └──┘ └┘ └┘ ┴ └─┘ └─┘ ┴
par └──┘ └┘ └┘ ┴ └─┘ └─┘ ┴
pid └┘ └┘ └┘ ┴ └─┘ └─┘ ┴
st ──────────────────────────┘└───────────────┘└──────────────────────────────────────┘└────────┘└──
111 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────────┘└─
112 end),
st ────────┘
113 one_mul := one_mul_aux n,
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
114 mul_one := λ a, by rw mul_comm; exact one_mul_aux n a,
id ┴ └──────┘ └─────────┘ ┴ ┴
src └─┘└──────┘ └────┘└─────────┘┴ ┴
typ ┴ └─┘└──────┘ └────┘└─────────┘┴┴┴┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └─────────────────────────────────┘
115 left_distrib := left_distrib_aux n,
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
116 right_distrib := λ a b c, by rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]; refl,
id ┴ ┴ ┴ └──────┘ └──────────────┘ └──────┘ ┴ └──────┘
src └──┘└──────┘└┘└──────────────┘└┘└──────┘└─┘ └┘└──────┘┴ └──┘
typ ┴ ┴ ┴ └──┘└──────┘└┘└──────────────┘└┘└──────┘└─┘┴└┘└──────┘┴ └──┘
doc └──┘ └┘ └┘ └─┘ └┘ ┴ └──┘
txt └──┘ └┘ └┘ └─┘ └┘ ┴ └──┘
par └──┘ └┘ └┘ └─┘ └┘ ┴ └──┘
pid └┘ └┘ └┘ └─┘ └┘ ┴
st └───────────┘└────────────────┘└────────────┘└────────┘┴└────┘
117 ..zmod.has_zero n,
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
118 ..zmod.has_one n,
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
119 ..zmod.has_neg n,
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
120 ..zmod.add_comm_semigroup n,
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
121 ..zmod.comm_semigroup n }
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
122
123 lemma val_cast_nat {n : ℕ+} (a : ℕ) : (a : zmod n).val = a % n :=
id └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └┘ ┴ └──┘ └─┘ ┴ ┴
typ └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └┘
124 begin
st └─────
125 induction a with a ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
126 { rw [nat.zero_mod]; refl },
id └──────────┘
src └──┘└──────────┘┴ └───┘
typ └──┘└──────────┘┴ └───┘
doc └──┘ ┴ └───┘
txt └──┘ ┴ └───┘
par └──┘ ┴ └───┘
pid └┘ ┴ ┴
st ───┘└──────────────┘┴└─────┘└┘└
127 { rw [succ_eq_add_one, nat.cast_add, add_val, ih],
id └─────────────┘ └──────────┘ └─────┘ └┘
src └──┘└─────────────┘└┘└──────────┘└┘└─────┘└┘ ┴
typ └──┘└─────────────┘└┘└──────────┘└┘└─────┘└┘└┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ──────────────────────┘└────────────┘└───────┘└──┘┴└─
128 show (a % n + ((0 + (1 % n)) % n)) % n = (a + 1) % n,
id ┴ ┴ ┴ ┴ ┴
src └───┘ ┴┴┴ ┴┴┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴┴┴ ┴ └──┘ ┴
typ └───┘ ┴┴┴ ┴┴┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴┴┴ ┴┴ └──┘ ┴┴
doc └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────┘└─
129 rw [zero_add, nat.mod_mod],
id └──────┘ └─────────┘
src └──┘└──────┘└┘└─────────┘┴
typ └──┘└──────┘└┘└─────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────┘└───────────┘└──
130 exact nat.modeq.modeq_add (nat.mod_mod a n) (nat.mod_mod 1 n) }
id └─────────────────┘ ┴ └─────────┘ ┴
src └────┘└─────────────────┘┴ ┴ ┴ └┘ └─────────┘└─┘ └┘
typ └────┘└─────────────────┘┴ ┴┴┴ └┘ └─────────┘└─┘┴└┘
doc └────┘ ┴ ┴ ┴ └┘ └─┘ └┘
txt └────┘ ┴ ┴ ┴ └┘ └─┘ └┘
par └────┘ ┴ ┴ ┴ └┘ └─┘ └┘
pid ┴ ┴ ┴ ┴ └┘ └─┘ ┴┴
st ─────────────────────────────────────────────────────────────────┘└─
131 end
st ──┘
132
133 lemma neg_val' {m : pnat} (n : zmod m) : (-n).val = (m - n.val) % m :=
id └──┘ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴
src └──┘ └──┘ ┴ └─┘ ┴ ┴ └──┘ ┴
typ └──┘ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴
doc └──┘
134 have ((-n).val + n.val) % m = (m - n.val + n.val) % m,
id ┴┴ └─┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
src ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴
typ ┴┴ └─┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
135 by { rw [←add_val, add_left_neg, nat.sub_add_cancel (le_of_lt n.is_lt), nat.mod_self], refl },
id └─────┘ └──────────┘ └────────────────┘ └──────┘ └─────┘ └──────────┘
src └───┘└─────┘└┘└──────────┘└┘└────────────────┘┴ └──────┘┴└─────┘└─┘└──────────┘┴ └───┘
typ └───┘└─────┘└┘└──────────┘└┘└────────────────┘┴ └──────┘┴└─────┘└─┘└──────────┘┴ └───┘
doc └───┘ └┘ └┘ ┴ ┴ └─┘ ┴ └───┘
txt └───┘ └┘ └┘ ┴ ┴ └─┘ ┴ └───┘
par └───┘ └┘ └┘ ┴ ┴ └─┘ ┴ └───┘
pid └─┘ └┘ └┘ ┴ ┴ └─┘ ┴ ┴
st └─────────────┘└────────────┘└─────────────────────────────────────┘└────────────┘└──────┘└┘
136 (nat.mod_eq_of_lt (fin.is_lt _)).symm.trans (nat.modeq.modeq_add_cancel_right rfl this)
id └──────────────┘ └───────┘ └──┘ └───┘ └──────────────────────────────┘ └─┘ └──┘
src └──────────────┘ └───────┘ └──┘ └───┘ └──────────────────────────────┘ └─┘
typ └──────────────┘ └───────┘ └──┘ └───┘ └──────────────────────────────┘ └─┘ └──┘
137
138 lemma neg_val {m : pnat} (n : zmod m) : (-n).val = if n = 0 then 0 else m - n.val :=
id └──┘ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
src └──┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └──┘
typ └──┘ └──┘ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
doc └──┘
139 begin
st └─────
140 rw neg_val',
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────┘└─
141 by_cases h : n = 0; simp [h],
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴└┘ └────┘ ┴
typ └───────┘ └─┘┴┴┴└┘ └────┘┴┴
doc └───────┘ └─┘ ┴ └┘ └────┘ ┴
txt └───────┘ └─┘ ┴ └┘ └────┘ ┴
par └───────┘ └─┘ ┴ └┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴┴ ┴┴ ┴
st ─────────────────────────────┘└─
142 cases n with n nlt; cases n; dsimp, { contradiction },
id ┴ ┴
src └────┘ └─────────┘ └────┘ └───┘ └────────────┘
typ └────┘┴└─────────┘ └────┘┴ └───┘ └────────────┘
doc └────┘ └─────────┘ └────┘ └───┘ └────────────┘
txt └────┘ └─────────┘ └────┘ └───┘ └────────────┘
par └────┘ └─────────┘ └────┘ └───┘ └────────────┘
pid ┴ └─────────┘ ┴ ┴
st ───────────────────────────────────┘└──┘└────────────┘└┘└
143 rw nat.mod_eq_of_lt,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
144 apply nat.sub_lt m.2 (nat.succ_pos _),
id └────────┘ ┴ └──────────┘
src └────┘└────────┘┴ └─┘ └──────────┘└─┘
typ └────┘└────────┘┴┴└─┘ └──────────┘└─┘
doc └────┘ ┴ └─┘ └─┘
txt └────┘ ┴ └─┘ └─┘
par └────┘ ┴ └─┘ └─┘
pid ┴ ┴ └─┘ └─┘
st ──────────────────────────────────────┘└─
145 end
st ──┘
146
147 lemma mk_eq_cast {n : ℕ+} {a : ℕ} (h : a < n) : (⟨a, h⟩ : zmod n) = (a : zmod n) :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
src └┘ ┴ ┴ └──┘ ┴ └──┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
doc └┘
148 fin.eq_of_veq (by rw [val_cast_nat, nat.mod_eq_of_lt h])
id └───────────┘ └──────────┘ └──────────────┘ ┴
src └───────────┘ └──┘└──────────┘└┘└──────────────┘┴ ┴
typ └───────────┘ └──┘└──────────┘└┘└──────────────┘┴┴┴
doc └──┘ └┘ ┴ ┴
txt └──┘ └┘ ┴ ┴
par └──┘ └┘ ┴ ┴
pid └┘ └┘ ┴ ┴
st └───────────────┘└──────────────────┘┴
149
150 @[simp] lemma cast_self_eq_zero {n : ℕ+} : ((n : ℕ) : zmod n) = 0 :=
id └┘ ┴ ┴ └──┘ ┴ ┴
src └┘ ┴ └──┘ ┴
typ └┘ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └┘
151 fin.eq_of_veq (show (n : zmod n).val = 0, by simp [val_cast_nat])
id └───────────┘ ┴ └──┘ ┴ └─┘ ┴ └──────────┘
src └───────────┘ └──┘ └─┘ ┴ └────┘└──────────┘┴
typ └───────────┘ ┴ └──┘ ┴ └─┘ ┴ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────────────┘
152
153 lemma val_cast_of_lt {n : ℕ+} {a : ℕ} (h : a < n) : (a : zmod n).val = a :=
id └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴
src └┘ ┴ ┴ └──┘ └─┘ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴
doc └┘
154 by rw [val_cast_nat, nat.mod_eq_of_lt h]
id └──────────┘ └──────────────┘ ┴
src └──┘└──────────┘└┘└──────────────┘┴ └─
typ └──┘└──────────┘└┘└──────────────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────────┘└──────────────────┘┴└
155
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
156 @[simp] lemma cast_mod_nat (n : ℕ+) (a : ℕ) : ((a % n : ℕ) : zmod n) = a :=
id └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ └──┘ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └┘
157 by conv {to_rhs, rw ← nat.mod_add_div a n}; simp
id └─────────────┘ ┴ ┴
src └────┘└────┘└┘└───┘└─────────────┘┴ ┴ ┴ └────
typ └────┘└────┘└┘└───┘└─────────────┘┴┴┴┴┴ └────
doc └────
txt └────┘└────┘└┘└───┘ ┴ ┴ ┴ └────
par └────┘└────┘└┘└───┘ ┴ ┴ ┴ └────
pid ┴└────────────┘ ┴ ┴ ┴ └
st └─────┘└────┘└────────────────────────┘└┘└─────
158
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
159 @[simp] lemma cast_mod_nat' {n : ℕ} (hn : 0 < n) (a : ℕ) : ((a % n : ℕ) : zmod ⟨n, hn⟩) = a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴
doc └──┘
160 cast_mod_nat _ _
id └──────────┘
src └──────────┘
typ └──────────┘
161
162 @[simp] lemma cast_val {n : ℕ+} (a : zmod n) : (a.val : zmod n) = a :=
id └┘ └──┘ ┴ ┴└──┘ └──┘ ┴ ┴ ┴
src └┘ └──┘ └──┘ └──┘ ┴
typ └┘ └──┘ ┴ ┴└──┘ └──┘ ┴ ┴ ┴
doc └──┘ └┘
163 by cases a; simp [mk_eq_cast]
id ┴ └────────┘
src └────┘ └────┘└────────┘└─
typ └────┘┴ └────┘└────────┘└─
doc └────┘ └────┘ └─
txt └────┘ └────┘ └─
par └────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └───────────────────────────
164
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
165 @[simp] lemma cast_mod_int (n : ℕ+) (a : ℤ) : ((a % (n : ℕ) : ℤ) : zmod n) = a :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ └──┘ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └┘
166 by conv {to_rhs, rw ← int.mod_add_div a n}; simp
id └─────────────┘ ┴ ┴
src └────┘└────┘└┘└───┘└─────────────┘┴ ┴ ┴ └────
typ └────┘└────┘└┘└───┘└─────────────┘┴┴┴┴┴ └────
doc └────
txt └────┘└────┘└┘└───┘ ┴ ┴ ┴ └────
par └────┘└────┘└┘└───┘ ┴ ┴ ┴ └────
pid ┴└────────────┘ ┴ ┴ ┴ └
st └─────┘└────┘└────────────────────────┘└┘└─────
167
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
168 @[simp] lemma cast_mod_int' {n : ℕ} (hn : 0 < n) (a : ℤ) :
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
169 ((a % (n : ℕ) : ℤ) : zmod ⟨n, hn⟩) = a := cast_mod_int _ _
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └──────────┘
src ┴ ┴ ┴ └──┘ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └──────────┘
170
171 lemma val_cast_int {n : ℕ+} (a : ℤ) : (a : zmod n).val = (a % (n : ℕ)).nat_abs :=
id └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─────┘
typ └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └┘
172 have h : nat_abs (a % (n : ℕ)) < n := int.coe_nat_lt.1 begin
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘┴
src └─────┘ ┴ ┴ ┴ └────────────┘┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘┴
st └─────
173 rw [nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))],
id └───────────────┘ └────────┘ └─────────────────────────┘ └───┘
src └──┘└───────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└─┘
typ └──┘└───────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└─┘
doc └──┘ ┴ └─┘ └─┘ └─┘
txt └──┘ ┴ └─┘ └─┘ └─┘
par └──┘ ┴ └─┘ └─┘ └─┘
pid └┘ ┴ └─┘ └─┘ └─┘
st ───────────────────────────────────────────────────────────────────────────┘└──
174 conv {to_rhs, rw ← abs_of_nonneg (int.coe_nat_nonneg n)},
id └───────────┘ └────────────────┘ ┴
src └────┘└────┘└┘└───┘└───────────┘┴ └────────────────┘┴ ┴┴
typ └────┘└────┘└┘└───┘└───────────┘┴ └────────────────┘┴┴┴┴
txt └────┘└────┘└┘└───┘ ┴ ┴ ┴┴
par └────┘└────┘└┘└───┘ ┴ ┴ ┴┴
pid ┴└────────────┘ ┴ ┴ └┘
st ───────┘└────┘└─────────────────────────────────────────┘└┘└
175 exact int.mod_lt _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)
id └────────┘ └─────────────────────────┘ └───┘
src └────┘└────────┘└─┘ └─────────────────────────┘└─┘└───┘└┘
typ └────┘└────────┘└─┘ └─────────────────────────┘└─┘└───┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ──────────────────────────────────────────────────────────┘
176 end,
st └─┘
177 int.coe_nat_inj $
id └─────────────┘
src └─────────────┘
typ └─────────────┘
178 by conv {to_lhs, rw [← cast_mod_int n a,
id └──────────┘ ┴ ┴
src └────┘└────┘└┘└────┘└──────────┘┴ ┴ └─
typ └────┘└────┘└┘└────┘└──────────┘┴┴┴┴└─
txt └────┘└────┘└┘└────┘ ┴ ┴ └─
par └────┘└────┘└┘└────┘ ┴ ┴ └─
pid ┴└─────────────┘ ┴ ┴ └─
st └─────┘└────┘└──────────────────────┘└─
179 ← nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
id └───────────────┘ └────────┘ └─────────────────────────┘ └───┘
src ─────┘└───────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ ─────┘└───────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
txt ─────┘ ┴ └─┘ └─┘ └───
par ─────┘ ┴ └─┘ └─┘ └───
pid ─────┘ ┴ └─┘ └─┘ └───
st ───────────────────────────────────────────────────────────────────────────┘└─
180 int.cast_coe_nat, val_cast_of_lt h] }
id └──────────────┘ └────────────┘ ┴
src ───┘└──────────────┘└┘└────────────┘┴ └┘└─
typ ───┘└──────────────┘└┘└────────────┘┴┴└┘└─
txt ───┘ └┘ ┴ └┘└─
par ───┘ └┘ ┴ └┘└─
pid ───┘ └┘ ┴ └─┘└
st ───────────────────┘└────────────────┘ ┴┴└
181
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
182 lemma coe_val_cast_int {n : ℕ+} (a : ℤ) : ((a : zmod n).val : ℤ) = a % (n : ℕ) :=
id └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
183 by rw [val_cast_int, int.nat_abs_of_nonneg (mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))]
id └──────────┘ └───────────────────┘ └────────┘ └─────────────────────────┘ └───┘
src └──┘└──────────┘└┘└───────────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ └──┘└──────────┘└┘└───────────────────┘┴ └────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
doc └──┘ └┘ ┴ └─┘ └─┘ └───
txt └──┘ └┘ ┴ └─┘ └─┘ └───
par └──┘ └┘ ┴ └─┘ └─┘ └───
pid └┘ └┘ ┴ └─┘ └─┘ └─┘└
st └───────────────┘└──────────────────────────────────────────────────────────────────────────┘┴└
184
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
185 lemma eq_iff_modeq_nat {n : ℕ+} {a b : ℕ} : (a : zmod n) = b ↔ a ≡ b [MOD n] :=
id └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
src └┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
typ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
doc └┘ ┴ └──┘ ┴
186 ⟨λ h, by have := fin.veq_of_eq h;
id ┴ └───────────┘ ┴
src └──────┘└───────────┘┴
typ ┴ └──────┘└───────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st └─────────────────────────
187 rwa [val_cast_nat, val_cast_nat] at this,
id └──────────┘ └──────────┘
src └───┘└──────────┘└┘└──────────┘└───────┘
typ └───┘└──────────┘└┘└──────────┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ──────┘└──────────┘└────────────┘┴└──────┘
188 λ h, fin.eq_of_veq $ by rwa [val_cast_nat, val_cast_nat]⟩
id ┴ └───────────┘ └──────────┘ └──────────┘
src └───────────┘ └───┘└──────────┘└┘└──────────┘┴
typ ┴ └───────────┘ └───┘└──────────┘└┘└──────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────────┘└────────────┘┴
189
190 lemma eq_iff_modeq_nat' {n : ℕ} (hn : 0 < n) {a b : ℕ} : (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [MOD n] :=
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
src ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
doc ┴ └──┘ ┴
191 eq_iff_modeq_nat
id └──────────────┘
src └──────────────┘
typ └──────────────┘
192
193 lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] :=
id └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └┘ ┴ └──┘ ┴ ┴ ┴ └───┘ ┴ ┴
typ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └┘
194 ⟨λ h, by have := fin.veq_of_eq h;
id ┴ └───────────┘ ┴
src └──────┘└───────────┘┴
typ ┴ └──────┘└───────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st └─────────────────────────
195 rwa [val_cast_int, val_cast_int, ← int.coe_nat_eq_coe_nat_iff,
id └──────────┘ └──────────┘ └────────────────────────┘
src └───┘└──────────┘└┘└──────────┘└──┘└────────────────────────┘└─
typ └───┘└──────────┘└┘└──────────┘└──┘└────────────────────────┘└─
doc └───┘ └┘ └──┘ └─
txt └───┘ └┘ └──┘ └─
par └───┘ └┘ └──┘ └─
pid └┘ └┘ └──┘ └─
st ──────┘└──────────┘└────────────┘└────────────────────────────┘└─
196 nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos)),
id └───────────────┘ └────────────┘ └─────────────────────────┘ └───┘
src ───┘└───────────────┘┴ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
typ ───┘└───────────────┘┴ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└───
doc ───┘ ┴ └─┘ └─┘ └───
txt ───┘ ┴ └─┘ └─┘ └───
par ───┘ ┴ └─┘ └─┘ └───
pid ───┘ ┴ └─┘ └─┘ └───
st ─────────────────────────────────────────────────────────────────────────────┘└─
197 nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero_iff_pos.2 n.pos))] at this,
id └───────────────┘ └────────────┘ └─────────────────────────┘ └───┘
src ───┘└───────────────┘┴ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└─────────┘
typ ───┘└───────────────┘┴ └────────────┘└─┘ └─────────────────────────┘└─┘└───┘└─────────┘
doc ───┘ ┴ └─┘ └─┘ └─────────┘
txt ───┘ ┴ └─┘ └─┘ └─────────┘
par ───┘ ┴ └─┘ └─┘ └─────────┘
pid ───┘ ┴ └─┘ └─┘ └─┘└──────┘
st ─────────────────────────────────────────────────────────────────────────────┘┴└──────┘
198 λ h : a % (n : ℕ) = b % (n : ℕ),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
199 by rw [← cast_mod_int n a, ← cast_mod_int n b, h]⟩
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └────┘└──────────┘┴ ┴ └──┘└──────────┘┴ ┴ └┘ ┴
typ └────┘└──────────┘┴┴┴┴└──┘└──────────┘┴┴┴┴└┘┴┴
doc └────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴
pid └──┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴
st └─────────────────────┘└──────────────────┘└─┘┴
200
201 lemma eq_iff_modeq_int' {n : ℕ} (hn : 0 < n) {a b : ℤ} :
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
202 (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [ZMOD (n : ℕ)] := eq_iff_modeq_int
id ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──────────────┘
src └──┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────────────┘
typ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──────────────┘
203
204 lemma eq_zero_iff_dvd_nat {n : ℕ+} {a : ℕ} : (a : zmod n) = 0 ↔ (n : ℕ) ∣ a :=
id └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
205 by rw [← @nat.cast_zero (zmod n), eq_iff_modeq_nat, nat.modeq.modeq_zero_iff]
id └───────────┘ └──┘ ┴ └──────────────┘ └──────────────────────┘
src └────┘ └───────────┘┴ └──┘┴ └─┘└──────────────┘└┘└──────────────────────┘└─
typ └────┘ └───────────┘┴ └──┘┴┴└─┘└──────────────┘└┘└──────────────────────┘└─
doc └────┘ ┴ ┴ └─┘ └┘ └─
txt └────┘ ┴ ┴ └─┘ └┘ └─
par └────┘ ┴ ┴ └─┘ └┘ └─
pid └──┘ ┴ ┴ └─┘ └┘ ┴└
st └────────────────────────────┘└────────────────┘└────────────────────────┘┴└
206
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
207 lemma eq_zero_iff_dvd_int {n : ℕ+} {a : ℤ} : (a : zmod n) = 0 ↔ ((n : ℕ) : ℤ) ∣ a :=
id └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
208 by rw [← @int.cast_zero (zmod n), eq_iff_modeq_int, int.modeq.modeq_zero_iff]
id └───────────┘ └──┘ ┴ └──────────────┘ └──────────────────────┘
src └────┘ └───────────┘┴ └──┘┴ └─┘└──────────────┘└┘└──────────────────────┘└─
typ └────┘ └───────────┘┴ └──┘┴┴└─┘└──────────────┘└┘└──────────────────────┘└─
doc └────┘ ┴ ┴ └─┘ └┘ └─
txt └────┘ ┴ ┴ └─┘ └┘ └─
par └────┘ ┴ ┴ └─┘ └┘ └─
pid └──┘ ┴ ┴ └─┘ └┘ ┴└
st └────────────────────────────┘└────────────────┘└────────────────────────┘┴└
209
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
210 instance (n : ℕ+) : fintype (zmod n) := fin.fintype _
id └┘ └─────┘ └──┘ ┴ └─────────┘
src └┘ └─────┘ └──┘ └─────────┘
typ └┘ └─────┘ └──┘ ┴ └─────────┘
doc └┘ └─────┘
211
212 instance decidable_eq (n : ℕ+) : decidable_eq (zmod n) := fin.decidable_eq _
id └┘ └──────────┘ └──┘ ┴ └──────────────┘
src └┘ └──────────┘ └──┘ └──────────────┘
typ └┘ └──────────┘ └──┘ ┴ └──────────────┘
doc └┘
213
214 instance (n : ℕ+) : has_repr (zmod n) := fin.has_repr _
id └┘ └──────┘ └──┘ ┴ └──────────┘
src └┘ └──────┘ └──┘ └──────────┘
typ └┘ └──────┘ └──┘ ┴ └──────────┘
doc └┘
215
216 lemma card_zmod (n : ℕ+) : fintype.card (zmod n) = n := fintype.card_fin n
id └┘ └──────────┘ └──┘ ┴ ┴ ┴ └──────────────┘ ┴
src └┘ └──────────┘ └──┘ ┴ └──────────────┘
typ └┘ └──────────┘ └──┘ ┴ ┴ ┴ └──────────────┘ ┴
doc └┘ └──────────┘
217
218 lemma le_div_two_iff_lt_neg {n : ℕ+} (hn : (n : ℕ) % 2 = 1)
id └┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴
doc └┘
219 {x : zmod n} (hx0 : x ≠ 0) : x.1 ≤ (n / 2 : ℕ) ↔ (n / 2 : ℕ) < (-x).1 :=
id └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
220 have hn2 : (n : ℕ) / 2 < n := nat.div_lt_of_lt_mul ((lt_mul_iff_one_lt_left n.pos).2 dec_trivial),
id ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └────────────────────┘ ┴└──┘ ┴ └─────────┘
src ┴ ┴ ┴ └──────────────────┘ └────────────────────┘ └──┘ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └────────────────────┘ ┴└──┘ ┴ └─────────┘
doc └─────────┘
221 have hn2' : (n : ℕ) - n / 2 = n / 2 + 1,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
222 by conv {to_lhs, congr, rw [← succ_sub_one n, succ_sub n.pos]};
id └──────────┘ ┴ └──────┘ └───┘
src └────┘└────┘└┘└───┘└┘└────┘└──────────┘┴ └┘└──────┘┴└───┘┴┴
typ └────┘└────┘└┘└───┘└┘└────┘└──────────┘┴┴└┘└──────┘┴└───┘┴┴
txt └────┘└────┘└┘└───┘└┘└────┘ ┴ └┘ ┴ ┴┴
par └────┘└────┘└┘└───┘└┘└────┘ ┴ └┘ ┴ ┴┴
pid ┴└────────────────────┘ ┴ └┘ ┴ └┘
st └─────┘└────┘└─────┘└────────────────────┘└──────────────┘ └┘└
223 rw [← two_mul_odd_div_two hn, two_mul, ← succ_add, nat.add_sub_cancel],
id └─────────────────┘ └┘ └─────┘ └──────┘ └────────────────┘
src └────┘└─────────────────┘┴ └┘└─────┘└──┘└──────┘└┘└────────────────┘┴
typ └────┘└─────────────────┘┴└┘└┘└─────┘└──┘└──────┘└┘└────────────────┘┴
doc └────┘ ┴ └┘ └──┘ └┘ ┴
txt └────┘ ┴ └┘ └──┘ └┘ ┴
par └────┘ ┴ └┘ └──┘ └┘ ┴
pid └──┘ ┴ └┘ └──┘ └┘ ┴
st ─────┘└──────────────────────┘└───────┘└──────────┘└──────────────────┘┴
224 have hxn : (n : ℕ) - x.val < n,
id ┴ ┴ ┴ ┴└──┘ ┴ ┴
src ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴└──┘ ┴ ┴
225 begin
st └─────
226 rw [nat.sub_lt_iff (le_of_lt x.2) (le_refl _), nat.sub_self],
id └────────────┘ └──────┘ ┴ └─────┘ └──────────┘
src └──┘└────────────┘┴ └──────┘┴ └──┘ └─────┘└───┘└──────────┘┴
typ └──┘└────────────┘┴ └──────┘┴┴└──┘ └─────┘└───┘└──────────┘┴
doc └──┘ ┴ ┴ └──┘ └───┘ ┴
txt └──┘ ┴ ┴ └──┘ └───┘ ┴
par └──┘ ┴ ┴ └──┘ └───┘ ┴
pid └┘ ┴ ┴ └──┘ └───┘ ┴
st ────────────────────────────────────────────────┘└────────────┘└──
227 rw ← zmod.cast_val x at hx0,
id └───────────┘ ┴
src └───┘└───────────┘┴ └─────┘
typ └───┘└───────────┘┴┴└─────┘
doc └───┘ ┴ └─────┘
txt └───┘ ┴ └─────┘
par └───┘ ┴ └─────┘
pid └─┘ ┴ └─────┘
st ──────────────────────────────┘└─
228 exact nat.pos_of_ne_zero (λ h, by simpa [h] using hx0)
id └────────────────┘ ┴ └─┘
src └────┘└────────────────┘┴ └──┘ ┴└─────┘ └──────┘ └─
typ └────┘└────────────────┘┴ └──┘ ┴└─────┘┴└──────┘└─┘└─
doc └────┘ ┴ └──┘ ┴└─────┘ └──────┘ └─
txt └────┘ ┴ └──┘ ┴└─────┘ └──────┘ └─
par └────┘ ┴ └──┘ ┴└─────┘ └──────┘ └─
pid ┴ ┴ └──┘ └──────┘ └──────┘ ┴└
st ────────────────────────────────────┘└──────────────────┘└─
229 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
230 by conv {to_rhs, rw [← nat.succ_le_iff, succ_eq_add_one, ← hn2', ← zero_add (- x), ← zmod.cast_self_eq_zero,
id └─────────────┘ └─────────────┘ └──┘ └──────┘ ┴ ┴ └────────────────────┘
src └────┘└────┘└┘└────┘└─────────────┘└┘└─────────────┘└──┘ └──┘└──────┘┴ ┴┴ └───┘└────────────────────┘└─
typ └────┘└────┘└┘└────┘└─────────────┘└┘└─────────────┘└──┘└──┘└──┘└──────┘┴ ┴┴┴└───┘└────────────────────┘└─
txt └────┘└────┘└┘└────┘ └┘ └──┘ └──┘ ┴ ┴ └───┘ └─
par └────┘└────┘└┘└────┘ └┘ └──┘ └──┘ ┴ ┴ └───┘ └─
pid ┴└─────────────┘ └┘ └──┘ └──┘ ┴ ┴ └───┘ └─
st └─────┘└────┘└─────────────────────┘└───────────────┘└──────┘└────────────────┘└────────────────────────┘└─
231 ← sub_eq_add_neg, ← zmod.cast_val x, ← nat.cast_sub (le_of_lt x.2),
id └────────────┘ └───────────┘ ┴ └──────────┘ └──────┘ ┴
src ───┘└────────────┘└──┘└───────────┘┴ └──┘└──────────┘┴ └──────┘┴ └────
typ ───┘└────────────┘└──┘└───────────┘┴┴└──┘└──────────┘┴ └──────┘┴┴└────
txt ───┘ └──┘ ┴ └──┘ ┴ ┴ └────
par ───┘ └──┘ ┴ └──┘ ┴ ┴ └────
pid ───┘ └──┘ ┴ └──┘ ┴ ┴ └────
st ─────────────────┘└─────────────────┘└─────────────────────────────┘└─
232 zmod.val_cast_nat, mod_eq_of_lt hxn, nat.sub_le_sub_left_iff (le_of_lt x.2)] }
id └───────────────┘ └──────────┘ └─┘ └─────────────────────┘ └──────┘ ┴
src ─┘└───────────────┘└┘└──────────┘┴ └┘└─────────────────────┘┴ └──────┘┴ └───┘└─
typ ─┘└───────────────┘└┘└──────────┘┴└─┘└┘└─────────────────────┘┴ └──────┘┴┴└───┘└─
txt ─┘ └┘ ┴ └┘ ┴ ┴ └───┘└─
par ─┘ └┘ ┴ └┘ ┴ ┴ └───┘└─
pid ─┘ └┘ ┴ └┘ ┴ ┴ └────┘└
st ──────────────────┘└────────────────┘└──────────────────────────────────────┘ ┴┴└
233
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
234 lemma ne_neg_self {n : ℕ+} (hn1 : (n : ℕ) % 2 = 1) {a : zmod n} (ha : a ≠ 0) : a ≠ -a :=
id └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src └┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └┘
235 λ h, have a.val ≤ n / 2 ↔ (n : ℕ) / 2 < (-a).val := le_div_two_iff_lt_neg hn1 ha,
id ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘ └───────────────────┘ └─┘ └┘
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └───────────────────┘
typ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─┘ └───────────────────┘ └─┘ └┘
236 by rwa [← h, ← not_lt, not_iff_self] at this
id ┴ └────┘ └──────────┘
src └─────┘ └──┘└────┘└┘└──────────┘└─────────
typ └─────┘┴└──┘└────┘└┘└──────────┘└─────────
doc └─────┘ └──┘ └┘ └─────────
txt └─────┘ └──┘ └┘ └─────────
par └─────┘ └──┘ └┘ └─────────
pid └──┘ └──┘ └┘ ┴└──────┘└
st └───────┘└────────┘└────────────┘┴└────────
237
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
238 @[simp] lemma cast_mul_right_val_cast {n m : ℕ+} (a : ℕ) :
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └──┘ └┘
239 ((a : zmod (m * n)).val : zmod m) = (a : zmod m) :=
id ┴ └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ ┴ └─┘ └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
240 zmod.eq_iff_modeq_nat.2 (by rw zmod.val_cast_nat;
id └───────────────────┘┴ └───────────────┘
src └───────────────────┘┴ └─┘└───────────────┘
typ └───────────────────┘┴ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └──────────────────────
241 exact nat.modeq.modeq_of_modeq_mul_right _ (nat.mod_mod _ _))
id └────────────────────────────────┘ └─────────┘
src └────┘└────────────────────────────────┘└─┘ └─────────┘└───┘
typ └────┘└────────────────────────────────┘└─┘ └─────────┘└───┘
doc └────┘ └─┘ └───┘
txt └────┘ └─┘ └───┘
par └────┘ └─┘ └───┘
pid ┴ └─┘ └───┘
st ─────────────────────────────────────────────────────────────┘
242
243 @[simp] lemma cast_mul_left_val_cast {n m : ℕ+} (a : ℕ) :
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └──┘ └┘
244 ((a : zmod (n * m)).val : zmod m) = (a : zmod m) :=
id ┴ └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ ┴ └─┘ └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
245 zmod.eq_iff_modeq_nat.2 (by rw zmod.val_cast_nat;
id └───────────────────┘┴ └───────────────┘
src └───────────────────┘┴ └─┘└───────────────┘
typ └───────────────────┘┴ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └──────────────────────
246 exact nat.modeq.modeq_of_modeq_mul_left _ (nat.mod_mod _ _))
id └───────────────────────────────┘ └─────────┘
src └────┘└───────────────────────────────┘└─┘ └─────────┘└───┘
typ └────┘└───────────────────────────────┘└─┘ └─────────┘└───┘
doc └────┘ └─┘ └───┘
txt └────┘ └─┘ └───┘
par └────┘ └─┘ └───┘
pid ┴ └─┘ └───┘
st ────────────────────────────────────────────────────────────┘
247
248 lemma cast_val_cast_of_dvd {n m : ℕ+} (h : (m : ℕ) ∣ n) (a : ℕ) :
id └┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴
doc └┘
249 ((a : zmod n).val : zmod m) = (a : zmod m) :=
id ┴ └──┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ └─┘ └──┘ ┴ └──┘
typ ┴ └──┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴
250 let ⟨k , hk⟩ := h in
id └─┘ ┴ ┴
typ └─┘ ┴ ┴
251 zmod.eq_iff_modeq_nat.2 (nat.modeq.modeq_of_modeq_mul_right k
id └───────────────────┘┴ └────────────────────────────────┘
src └───────────────────┘┴ └────────────────────────────────┘
typ └───────────────────┘┴ └────────────────────────────────┘
252 (by rw [← hk, zmod.val_cast_nat]; exact nat.mod_mod _ _))
id └┘ └───────────────┘ └─────────┘
src └────┘ └┘└───────────────┘┴ └────┘└─────────┘└──┘
typ └────┘└┘└┘└───────────────┘┴ └────┘└─────────┘└──┘
doc └────┘ └┘ ┴ └────┘ └──┘
txt └────┘ └┘ ┴ └────┘ └──┘
par └────┘ └┘ ┴ └────┘ └──┘
pid └──┘ └┘ ┴ ┴ └──┘
st └───────┘└─────────────────┘┴└─────────────────────┘
253
254 def units_equiv_coprime {n : ℕ+} : units (zmod n) ≃ {x : zmod n // nat.coprime x.1 n} :=
id └┘ └───┘ └──┘ ┴ ┴ ┴ └──┘ ┴ └─────────┘ ┴┴ ┴
src └┘ └───┘ └──┘ ┴ ┴ └──┘ └─────────┘ ┴
typ └┘ └───┘ └──┘ ┴ ┴ ┴ └──┘ ┴ └─────────┘ ┴┴ ┴
doc └┘ ┴
255 { to_fun := λ x, ⟨x, nat.modeq.coprime_of_mul_modeq_one (x⁻¹).1.1 begin
id ┴ ┴ └────────────────────────────────┘ ┴└┘ ┴ ┴
src └────────────────────────────────┘ └┘ ┴ ┴
typ ┴ ┴ └────────────────────────────────┘ ┴└┘ ┴ ┴
st └─────
256 have := units.ext_iff.1 (mul_right_inv x),
id └───────────┘ └───────────┘ ┴
src └──────┘└───────────┘└─┘ └───────────┘┴ ┴
typ └──────┘└───────────┘└─┘ └───────────┘┴┴┴
doc └──────┘ └─┘ ┴ ┴
txt └──────┘ └─┘ ┴ ┴
par └──────┘ └─┘ ┴ ┴
pid └───┘└─┘ └─┘ ┴ ┴
st ────────────────────────────────────────────┘└─
257 rwa [← zmod.cast_val ((1 : units (zmod n)) : zmod n), units.coe_one, zmod.one_val,
id └───────────┘ └───┘ └──┘ ┴ └───────────┘ └──────────┘
src └─────┘└───────────┘┴ └──┘└───┘┴ └──┘┴ └───┘ ┴ └─┘└───────────┘└┘└──────────┘└─
typ └─────┘└───────────┘┴ └──┘└───┘┴ └──┘┴┴└───┘ ┴ └─┘└───────────┘└┘└──────────┘└─
doc └─────┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └─┘ └┘ └─
txt └─────┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └─┘ └┘ └─
par └─────┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └─┘ └┘ └─
pid └──┘ ┴ └──┘ ┴ ┴ └───┘ ┴ └─┘ └┘ └─
st ───────────────────────────────────────────────────────┘└─────────────┘└────────────┘└─
258 ← zmod.cast_val ((x * x⁻¹ : units (zmod n)) : zmod n),
id └───────────┘ ┴ ┴└┘ └───┘ └──┘ ┴
src ───────┘└───────────┘┴ ┴┴┴ └┘└─┘└───┘┴ └──┘┴ └───┘ ┴ └──
typ ───────┘└───────────┘┴ ┴┴┴┴└┘└─┘└───┘┴ └──┘┴┴└───┘ ┴ └──
doc ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └──
txt ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └──
par ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └──
pid ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └──
st ──────────────────────────────────────────────────────────┘└─
259 units.coe_mul, zmod.mul_val, zmod.cast_mod_nat, zmod.cast_mod_nat,
id └───────────┘ └──────────┘ └───────────────┘ └───────────────┘
src ─────┘└───────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────────┘└─
typ ─────┘└───────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────────┘└─
doc ─────┘ └┘ └┘ └┘ └─
txt ─────┘ └┘ └┘ └┘ └─
par ─────┘ └┘ └┘ └┘ └─
pid ─────┘ └┘ └┘ └┘ └─
st ──────────────────┘└────────────┘└─────────────────┘└─────────────────┘└─
260 zmod.eq_iff_modeq_nat] at this
id └───────────────────┘
src ─────┘└───────────────────┘└─────────
typ ─────┘└───────────────────┘└─────────
doc ─────┘ └─────────
txt ─────┘ └─────────
par ─────┘ └─────────
pid ─────┘ ┴└──────┘└
st ──────────────────────────┘┴└────────
261 end⟩,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
262 inv_fun := λ x,
id ┴
typ ┴
263 have x.val * ↑(gcd_a ((x.val).val) ↑n) = 1,
id ┴└──┘ ┴ ┴ └───┘ ┴└──┘ └─┘ ┴┴ ┴
src └──┘ ┴ ┴ └───┘ └──┘ └─┘ ┴ ┴
typ ┴└──┘ ┴ ┴ └───┘ ┴└──┘ └─┘ ┴┴ ┴
doc └───┘
264 by rw [← zmod.cast_val x.1, ← int.cast_coe_nat, ← int.cast_one, ← int.cast_mul,
id └───────────┘ ┴ └──────────────┘ └──────────┘ └──────────┘
src └────┘└───────────┘┴ └────┘└──────────────┘└──┘└──────────┘└──┘└──────────┘└─
typ └────┘└───────────┘┴┴└────┘└──────────────┘└──┘└──────────┘└──┘└──────────┘└─
doc └────┘ ┴ └────┘ └──┘ └──┘ └─
txt └────┘ ┴ └────┘ └──┘ └──┘ └─
par └────┘ ┴ └────┘ └──┘ └──┘ └─
pid └──┘ ┴ └────┘ └──┘ └──┘ └─
st └────────────────────┘└────────────────────┘└──────────────┘└──────────────┘└─
265 zmod.eq_iff_modeq_int, ← int.coe_nat_one, ← (show nat.gcd _ _ = _, from x.2)];
id └───────────────────┘ └─────────────┘ └─────┘ ┴ ┴
src ─────────┘└───────────────────┘└──┘└─────────────┘└──┘ ┴└─────┘└───┘┴└───────┘ └──┘
typ ─────────┘└───────────────────┘└──┘└─────────────┘└──┘ ┴└─────┘└───┘┴└───────┘┴└──┘
doc ─────────┘ └──┘ └──┘ ┴ └───┘ └───────┘ └──┘
txt ─────────┘ └──┘ └──┘ ┴ └───┘ └───────┘ └──┘
par ─────────┘ └──┘ └──┘ ┴ └───┘ └───────┘ └──┘
pid ─────────┘ └──┘ └──┘ ┴ └───┘ └───────┘ └──┘
st ──────────────────────────────┘└─────────────────┘└──────────────────────────────────┘┴└─
266 simpa using int.modeq.gcd_a_modeq x.1.1 n,
id └───────────────────┘ ┴ ┴
src └──────────┘└───────────────────┘┴ └───┘
typ └──────────┘└───────────────────┘┴┴└───┘┴
doc └──────────┘ ┴ └───┘
txt └──────────┘ ┴ └───┘
par └──────────┘ ┴ └───┘
pid ┴└────┘ ┴ └───┘
st ────────────────────────────────────────────────┘
267 ⟨x.1, gcd_a x.1.1 n, this, by simpa [mul_comm] using this⟩,
id ┴┴ └───┘ ┴┴ ┴ ┴ └──┘ └──────┘ └──┘
src ┴ └───┘ ┴ ┴ └─────┘└──────┘└──────┘
typ ┴┴ └───┘ ┴┴ ┴ ┴ └──┘ └─────┘└──────┘└──────┘└──┘
doc └───┘ └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └──────────────────────────┘
268 left_inv := λ ⟨_, _, _, _⟩, units.ext rfl,
id ┴ └───────┘ └─┘
src └───────┘ └─┘
typ ┴ └───────┘ └─┘
269 right_inv := λ ⟨_, _⟩, rfl }
id ┴ └─┘
src └─┘
typ ┴ └─┘
270
271 /-- `val_min_abs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
272 The result will be in the interval `(-n/2, n/2]` -/
273 def val_min_abs {n : ℕ+} (x : zmod n) : ℤ :=
id └┘ └──┘ ┴ ┴
src └┘ └──┘ ┴
typ └┘ └──┘ ┴ ┴
doc └┘
274 if x.val ≤ n / 2 then x.val else x.val - n
id ┴└──┘ ┴ ┴ ┴ ┴└──┘ ┴└──┘ ┴ ┴
src └──┘ ┴ ┴ └──┘ └──┘ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴└──┘ ┴└──┘ ┴ ┴
275
276 @[simp] lemma coe_val_min_abs {n : ℕ+} (x : zmod n) :
id └┘ └──┘ ┴
src └┘ └──┘
typ └┘ └──┘ ┴
doc └──┘ └┘
277 (x.val_min_abs : zmod n) = x :=
id ┴└──────────┘ └──┘ ┴ ┴ ┴
src └──────────┘ └──┘ ┴
typ ┴└──────────┘ └──┘ ┴ ┴ ┴
doc └──────────┘
278 by simp [zmod.val_min_abs]; split_ifs; simp
id └──────────────┘
src └────┘└──────────────┘┴ └───────┘ └────
typ └────┘└──────────────┘┴ └───────┘ └────
doc └────┘└──────────────┘┴ └───────┘ └────
txt └────┘ ┴ └───────┘ └────
par └────┘ ┴ └───────┘ └────
pid ┴┴ ┴ └
st └─────────────────────────────────────────
279
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
280 lemma nat_abs_val_min_abs_le {n : ℕ+} (x : zmod n) : x.val_min_abs.nat_abs ≤ n / 2 :=
id └┘ └──┘ ┴ ┴└──────────┘└──────┘ ┴ ┴ ┴
src └┘ └──┘ └──────────┘└──────┘ ┴ ┴
typ └┘ └──┘ ┴ ┴└──────────┘└──────┘ ┴ ┴ ┴
doc └┘ └──────────┘
281 have (x.val - n : ℤ) ≤ 0, from sub_nonpos.2 $ int.coe_nat_le.2 $ le_of_lt x.2,
id ┴└──┘ ┴ ┴ ┴ ┴ └────────┘┴ └────────────┘┴ └──────┘ ┴┴
src └──┘ ┴ ┴ ┴ └────────┘┴ └────────────┘┴ └──────┘ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴ └────────┘┴ └────────────┘┴ └──────┘ ┴┴
282 begin
st └─────
283 rw zmod.val_min_abs,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘└──────────────┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
284 split_ifs with h,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid ┴└────┘
st ─────────────────┘└─
285 { exact h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
286 { rw [← int.coe_nat_le, int.of_nat_nat_abs_of_nonpos this, neg_sub],
id └────────────┘ └──────────────────────────┘ └──┘ └─────┘
src └────┘└────────────┘└┘└──────────────────────────┘┴ └┘└─────┘┴
typ └────┘└────────────┘└┘└──────────────────────────┘┴└──┘└┘└─────┘┴
doc └────┘ └┘ ┴ └┘ ┴
txt └────┘ └┘ ┴ └┘ ┴
par └────┘ └┘ ┴ └┘ ┴
pid └──┘ └┘ ┴ └┘ ┴
st ───────────────────────┘└─────────────────────────────────┘└───────┘└──
287 conv_lhs { congr, rw [coe_coe, ← nat.mod_add_div n 2, int.coe_nat_add, int.coe_nat_mul,
id └─────┘ └─────────────┘ ┴ └─────────────┘ └─────────────┘
src └─────────┘└───┘└┘└──┘└─────┘└──┘└─────────────┘┴ └──┘└─────────────┘└┘└─────────────┘└─
typ └─────────┘└───┘└┘└──┘└─────┘└──┘└─────────────┘┴┴└──┘└─────────────┘└┘└─────────────┘└─
doc └─────┘
txt └─────────┘└───┘└┘└──┘ └──┘ ┴ └──┘ └┘ └─
par └─────────┘└───┘└┘└──┘ └──┘ ┴ └──┘ └┘ └─
pid ┴└───────────┘ └──┘ ┴ └──┘ └┘ └─
st ─────────────┘└────┘└───────────┘└────────────────────┘└────────────────┘└───────────────┘└─
288 int.coe_nat_bit0, int.coe_nat_one] },
id └──────────────┘ └─────────────┘
src ─────┘└──────────────┘└┘└─────────────┘└┘┴
typ ─────┘└──────────────┘└┘└─────────────┘└┘┴
txt ─────┘ └┘ └┘┴
par ─────┘ └┘ └┘┴
pid ─────┘ └┘ └─┘
st ─────────────────────┘└───────────────┘ ┴└┘└
289 rw ← sub_nonneg,
id └────────┘
src └───┘└────────┘
typ └───┘└────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────────────┘└─
290 suffices : (0 : ℤ) ≤ x.val - ((n % 2 : ℕ) + (n / 2 : ℕ)),
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └──┘ └┘┴┴└───┘┴┴┴ ┴┴└───┘ └┘┴┴ ┴┴└───┘ └┘
typ └─────────┘ └──┘ └┘┴┴└───┘┴┴┴ ┴┴└───┘ └┘┴┴ ┴┴┴└───┘ └┘
doc └─────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └┘
txt └─────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └┘
par └─────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └┘
pid └───────┘└┘ └──┘ └┘ ┴ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └┘
st ───────────────────────────────────────────────────────────┘└─
291 { exact le_trans this (le_of_eq $ by ring) },
id └──────┘ └──┘ └──────┘
src └────┘└──────┘┴ ┴ └──────┘┴ ┴ ┴└──┘└┘
typ └────┘└──────┘┴└──┘┴ └──────┘┴ ┴ ┴└──┘└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴└──┘└┘
txt └────┘ ┴ ┴ ┴ ┴ ┴└──┘└┘
par └────┘ ┴ ┴ ┴ ┴ ┴└──┘└┘
pid ┴ ┴ ┴ ┴ ┴ └────┘┴
st ─────┘└────────────────────────────────┘└───┘└┘└┘└
292 exact sub_nonneg.2 (by rw [← int.coe_nat_add, int.coe_nat_le];
id └────────┘ └─────────────┘ └────────────┘
src └────┘└────────┘└─┘ ┴└────┘└─────────────┘└┘└────────────┘┴└─
typ └────┘└────────┘└─┘ ┴└────┘└─────────────┘└┘└────────────┘┴└─
doc └────┘ └─┘ ┴└────┘ └┘ ┴└─
txt └────┘ └─┘ ┴└────┘ └┘ ┴└─
par └────┘ └─┘ ┴└────┘ └┘ ┴└─
pid ┴ └─┘ └─────┘ └┘ └──
st ─────────────────────────┘└────────────────────┘└──────────────┘┴└─
293 exact calc (n : ℕ) % 2 + n / 2 ≤ 1 + n / 2 :
id ┴
src ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────
typ ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴┴┴ └────
doc ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────
txt ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────
par ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────
pid ───────────┘ ┴ └─┘ └┘ └─┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────
st ───────────────────────────────────────────────────
294 add_le_add (nat.le_of_lt_succ (nat.mod_lt _ dec_trivial)) (le_refl _)
id └────────┘ └───────────────┘ └────────┘ └─────────┘ └─────┘
src ───────┘└────────┘┴ └───────────────┘┴ └────────┘└─┘└─────────┘└─┘ └─────┘└───
typ ───────┘└────────┘┴ └───────────────┘┴ └────────┘└─┘└─────────┘└─┘ └─────┘└───
doc ───────┘ ┴ ┴ └─┘└─────────┘└─┘ └───
txt ───────┘ ┴ ┴ └─┘ └─┘ └───
par ───────┘ ┴ ┴ └─┘ └─┘ └───
pid ───────┘ ┴ ┴ └─┘ └─┘ └───
st ──────────────────────────────────────────────────────────────────────────────
295 ... ≤ x.val : by rw add_comm; exact nat.succ_le_of_lt (lt_of_not_ge h)) }
id └───┘ └──────┘ └───────────────┘ └──────────┘ ┴
src ───────────┘ ┴└───┘└─┘ ┴└─┘└──────┘└──────┘└───────────────┘┴ └──────────┘┴ └─┘
typ ───────────┘ ┴└───┘└─┘ ┴└─┘└──────┘└──────┘└───────────────┘┴ └──────────┘┴┴└─┘
doc ───────────┘ ┴ └─┘ ┴└─┘ └──────┘ ┴ ┴ └─┘
txt ───────────┘ ┴ └─┘ ┴└─┘ └──────┘ ┴ ┴ └─┘
par ───────────┘ ┴ └─┘ ┴└─┘ └──────┘ ┴ ┴ └─┘
pid ───────────┘ ┴ └─┘ └──┘ └──────┘ ┴ ┴ └┘┴
st ───────────────────────┘└────────────────────────────────────────────────────┘└┘└─
296 end
st ──┘
297
298 @[simp] lemma val_min_abs_zero {n : ℕ+} : (0 : zmod n).val_min_abs = 0 :=
id └┘ └──┘ ┴ └─────────┘ ┴
src └┘ └──┘ └─────────┘ ┴
typ └┘ └──┘ ┴ └─────────┘ ┴
doc └──┘ └┘ └─────────┘
299 by simp [zmod.val_min_abs]
id └──────────────┘
src └────┘└──────────────┘└─
typ └────┘└──────────────┘└─
doc └────┘└──────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────────
300
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
301 @[simp] lemma val_min_abs_eq_zero {n : ℕ+} (x : zmod n) :
id └┘ └──┘ ┴
src └┘ └──┘
typ └┘ └──┘ ┴
doc └──┘ └┘
302 x.val_min_abs = 0 ↔ x = 0 :=
id ┴└──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ ┴└──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
303 ⟨λ h, begin
id ┴
typ ┴
st └─────
304 dsimp [zmod.val_min_abs] at h,
id └──────────────┘
src └─────┘└──────────────┘└────┘
typ └─────┘└──────────────┘└────┘
doc └─────┘└──────────────┘└────┘
txt └─────┘ └────┘
par └─────┘ └────┘
pid ┴┴ ┴┴└──┘
st ──────────────────────────────┘└─
305 split_ifs at h,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └───┘
st ───────────────┘└─
306 { exact fin.eq_of_veq (by simp * at *) },
id └───────────┘
src └────┘└───────────┘┴ ┴└─────────┘└┘
typ └────┘└───────────┘┴ ┴└─────────┘└┘
doc └────┘ ┴ ┴└─────────┘└┘
txt └────┘ ┴ ┴└─────────┘└┘
par └────┘ ┴ ┴└─────────┘└┘
pid ┴ ┴ └───────────┘┴
st ───┘└─────────────────────┘└──────────┘└┘└┘└
307 { exact absurd h (mt sub_eq_zero.1 (ne_of_lt $ int.coe_nat_lt.2 x.2)) }
id └────┘ ┴ └┘ └─────────┘ └──────┘ └────────────┘ ┴
src └────┘└────┘┴ ┴ └┘┴└─────────┘└─┘ └──────┘┴ ┴└────────────┘└─┘ └───┘
typ └────┘└────┘┴┴┴ └┘┴└─────────┘└─┘ └──────┘┴ ┴└────────────┘└─┘┴└───┘
doc └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘
txt └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘
par └────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └───┘
pid ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └──┘┴
st ───────────────────────────────────────────────────────────────────────┘└─
308 end, λ hx0, hx0.symm ▸ zmod.val_min_abs_zero⟩
id └─┘ └─┘└───┘ ┴ └───────────────────┘
src └───┘ ┴ └───────────────────┘
typ └─┘ └─┘└───┘ ┴ └───────────────────┘
st ──┘
309
310 lemma cast_nat_abs_val_min_abs {n : ℕ+} (a : zmod n) :
id └┘ └──┘ ┴
src └┘ └──┘
typ └┘ └──┘ ┴
doc └┘
311 (a.val_min_abs.nat_abs : zmod n) = if a.val ≤ (n : ℕ) / 2 then a else -a :=
id ┴└──────────┘└──────┘ └──┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src └──────────┘└──────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴└──────────┘└──────┘ └──┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └──────────┘
312 have (a.val : ℤ) + -n ≤ 0, by erw [sub_nonpos, int.coe_nat_le]; exact le_of_lt a.2,
id ┴└──┘ ┴ ┴ ┴┴ ┴ └────────┘ └────────────┘ └──────┘ ┴
src └──┘ ┴ ┴ ┴ ┴ └───┘└────────┘└┘└────────────┘┴ └────┘└──────┘┴ └┘
typ ┴└──┘ ┴ ┴ ┴┴ ┴ └───┘└────────┘└┘└────────────┘┴ └────┘└──────┘┴┴└┘
doc └───┘ └┘ ┴ └────┘ ┴ └┘
txt └───┘ └┘ ┴ └────┘ ┴ └┘
par └───┘ └┘ ┴ └────┘ ┴ └┘
pid └┘ └┘ ┴ ┴ ┴ └┘
st └──────────────┘└──────────────┘┴└──────────────────┘
313 begin
st └─────
314 dsimp [zmod.val_min_abs],
id └──────────────┘
src └─────┘└──────────────┘┴
typ └─────┘└──────────────┘┴
doc └─────┘└──────────────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────────────┘└─
315 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
316 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
317 { erw [← int.cast_coe_nat, int.of_nat_nat_abs_of_nonpos this],
id └──────────────┘ └──────────────────────────┘ └──┘
src └─────┘└──────────────┘└┘└──────────────────────────┘┴ ┴
typ └─────┘└──────────────┘└┘└──────────────────────────┘┴└──┘┴
doc └─────┘ └┘ ┴ ┴
txt └─────┘ └┘ ┴ ┴
par └─────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st ──────────────────────────┘└─────────────────────────────────┘└──
318 simp }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
319 end
st ──┘
320
321 @[simp] lemma nat_abs_val_min_abs_neg {n : ℕ+} (a : zmod n) :
id └┘ └──┘ ┴
src └┘ └──┘
typ └┘ └──┘ ┴
doc └──┘ └┘
322 (-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs :=
id ┴┴ └─────────┘ └─────┘ ┴ ┴└──────────┘└──────┘
src ┴ └─────────┘ └─────┘ ┴ └──────────┘└──────┘
typ ┴┴ └─────────┘ └─────┘ ┴ ┴└──────────┘└──────┘
doc └─────────┘ └──────────┘
323 if haa : -a = a then by rw [haa]
id └┘ ┴┴ ┴ ┴ └─┘
src └┘ ┴ ┴ └──┘ └┘
typ └┘ ┴┴ ┴ ┴ └──┘└─┘└┘
doc └──┘ └┘
txt └──┘ └┘
par └──┘ └┘
pid └┘ ┴┴
st └──────┘┴┴
324 else
325 have hpa : (n : ℕ) - a.val ≤ n / 2 ↔ (n : ℕ) / 2 < a.val,
id └──┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
src └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
326 from suffices (((n : ℕ) % 2) + 2 * (n / 2)) - a.val ≤ (n : ℕ) / 2 ↔ (n : ℕ) / 2 < a.val,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
327 by rwa [nat.mod_add_div] at this,
id └─────────────┘
src └───┘└─────────────┘└───────┘
typ └───┘└─────────────┘└───────┘
doc └───┘ └───────┘
txt └───┘ └───────┘
par └───┘ └───────┘
pid └┘ ┴└──────┘
st └───────────────────┘┴└──────┘
328 begin
st └─────
329 rw [nat.sub_le_iff, two_mul, ← add_assoc, nat.add_sub_cancel],
id └────────────┘ └─────┘ └───────┘ └────────────────┘
src └──┘└────────────┘└┘└─────┘└──┘└───────┘└┘└────────────────┘┴
typ └──┘└────────────┘└┘└─────┘└──┘└───────┘└┘└────────────────┘┴
doc └──┘ └┘ └──┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ ┴
st ─────────────────────┘└───────┘└───────────┘└──────────────────┘└──
330 cases (n : ℕ).mod_two_eq_zero_or_one with hn0 hn1,
id ┴
src └────┘ └─┘ └───────────────────────────────────┘
typ └────┘ ┴└─┘ └───────────────────────────────────┘
doc └────┘ └─┘ └───────────────────────────────────┘
txt └────┘ └─┘ └───────────────────────────────────┘
par └────┘ └─┘ └───────────────────────────────────┘
pid ┴ └─┘ └─────────────────────┘└────────────┘
st ────────────────────────────────────────────────────┘└─
331 { split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ─────┘└───┘└─
332 { exact λ h, lt_of_le_of_ne (le_trans (nat.le_add_left _ _) h)
id └────────────┘ └──────┘ └─────────────┘
src └────┘ └──┘└────────────┘┴ └──────┘┴ └─────────────┘└────┘ └─
typ └────┘ └──┘└────────────┘┴ └──────┘┴ └─────────────┘└────┘ └─
doc └────┘ └──┘ ┴ ┴ └────┘ └─
txt └────┘ └──┘ ┴ ┴ └────┘ └─
par └────┘ └──┘ ┴ ┴ └────┘ └─
pid ┴ └──┘ ┴ ┴ └────┘ └─
st ───────┘└────────────────────────────────────────────────────────────
333 begin
src ─────────┘ └
typ ─────────┘ └
doc ─────────┘ └
txt ─────────┘ └
par ─────────┘ └
pid ─────────┘ └
st ─────────┘└─────
334 assume hna,
src ───────────┘└────────┘└─
typ ───────────┘└────────┘└─
doc ───────────┘└────────┘└─
txt ───────────┘└────────┘└─
par ───────────┘└────────┘└─
pid ────────────────────────
st ─────────────────────┘└─
335 rw [← zmod.cast_val a, ← hna, neg_eq_iff_add_eq_zero, ← nat.cast_add,
id └───────────┘ ┴ └─┘ └────────────────────┘ └──────────┘
src ───────────┘└────┘└───────────┘┴ └──┘ └┘└────────────────────┘└──┘└──────────┘└─
typ ───────────┘└────┘└───────────┘┴┴└──┘└─┘└┘└────────────────────┘└──┘└──────────┘└─
doc ───────────┘└────┘ ┴ └──┘ └┘ └──┘ └─
txt ───────────┘└────┘ ┴ └──┘ └┘ └──┘ └─
par ───────────┘└────┘ ┴ └──┘ └┘ └──┘ └─
pid ─────────────────┘ ┴ └──┘ └┘ └──┘ └─
st ────────────────────────────────┘└─────┘└──────────────────────┘└──────────────┘└─
336 zmod.eq_zero_iff_dvd_nat, ← two_mul, ← zero_add (2 * _), ← hn0,
id └──────────────────────┘ └─────┘ └──────┘ ┴ └─┘
src ─────────────┘└──────────────────────┘└──┘└─────┘└──┘└──────┘┴ └┘┴└─────┘ └─
typ ─────────────┘└──────────────────────┘└──┘└─────┘└──┘└──────┘┴ └┘┴└─────┘└─┘└─
doc ─────────────┘ └──┘ └──┘ ┴ └┘ └─────┘ └─
txt ─────────────┘ └──┘ └──┘ ┴ └┘ └─────┘ └─
par ─────────────┘ └──┘ └──┘ ┴ └┘ └─────┘ └─
pid ─────────────┘ └──┘ └──┘ ┴ └┘ └─────┘ └─
st ─────────────────────────────────────┘└─────────┘└──────────────────┘└─────┘└─
337 nat.mod_add_div] at haa,
id └─────────────┘
src ─────────────┘└─────────────┘└──────┘└─
typ ─────────────┘└─────────────┘└──────┘└─
doc ─────────────┘ └──────┘└─
txt ─────────────┘ └──────┘└─
par ─────────────┘ └──────┘└─
pid ─────────────┘ └─────────
st ────────────────────────────┘┴└─────┘└─
338 exact haa (dvd_refl _)
id └─┘ └──────┘
src ─────────────────┘ ┴ └──────┘└───
typ ─────────────────┘└─┘┴ └──────┘└───
doc ─────────────────┘ ┴ └───
txt ─────────────────┘ ┴ └───
par ─────────────────┘ ┴ └───
pid ─────────────────┘ ┴ └───
st ───────────────────────────────────
339 end },
src ─────────────┘
typ ─────────────┘
doc ─────────────┘
txt ─────────────┘
par ─────────────┘
pid ────────────┘┴
st ─────────┘└─┘┴└┘└
340 { rw [hn0, zero_add], exact le_of_lt } },
id └─┘ └──────┘ └──────┘
src └──┘ └┘└──────┘┴ └────┘└──────┘┴
typ └──┘└─┘└┘└──────┘┴ └────┘└──────┘┴
doc └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ ┴ ┴ ┴
st ──────────────┘└────────┘└────────────────┘└──┘└
341 { rw [hn1, add_comm, nat.succ_le_iff] }
id └─┘ └──────┘ └─────────────┘
src └──┘ └┘└──────┘└┘└─────────────┘└┘
typ └──┘└─┘└┘└──────┘└┘└─────────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ────────────┘└────────┘└───────────────┘┴┴└─
342 end,
st ────┘
343 have ha0 : ¬ a = 0, from λ ha0, by simp * at *,
id ┴ ┴ ┴ └─┘
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴ └─┘ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴┴┴└──┘
st └──────────┘
344 begin
st └─────
345 dsimp [zmod.val_min_abs],
id └──────────────┘
src └─────┘└──────────────┘┴
typ └─────┘└──────────────┘┴
doc └─────┘└──────────────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ─────────────────────────┘└─
346 rw [← not_le] at hpa,
id └────┘
src └────┘└────┘└──────┘
typ └────┘└────┘└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid └──┘ ┴└─────┘
st ─────────────┘┴└─────┘└─
347 simp only [if_neg ha0, zmod.neg_val, hpa, int.coe_nat_sub (le_of_lt a.2)],
id └────┘ └─┘ └──────────┘ └─┘ └─────────────┘ └──────┘ ┴
src └─────────┘└────┘┴ └┘└──────────┘└┘ └┘└─────────────┘┴ └──────┘┴ └──┘
typ └─────────┘└────┘┴└─┘└┘└──────────┘└┘└─┘└┘└─────────────┘┴ └──────┘┴┴└──┘
doc └─────────┘ ┴ └┘ └┘ └┘ ┴ ┴ └──┘
txt └─────────┘ ┴ └┘ └┘ └┘ ┴ ┴ └──┘
par └─────────┘ ┴ └┘ └┘ └┘ ┴ ┴ └──┘
pid ┴└──┘└┘ ┴ └┘ └┘ └┘ ┴ ┴ └──┘
st ──────────────────────────────────────────────────────────────────────────┘└─
348 split_ifs,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st ──────────┘└─
349 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
350 { rw [← int.nat_abs_neg], simp }
id └─────────────┘
src └────┘└─────────────┘┴ └───┘
typ └────┘└─────────────┘┴ └───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid └──┘ ┴ ┴
st ────────────────────────┘└──────┘└─
351 end
st ──┘
352
353 lemma val_eq_ite_val_min_abs {n : ℕ+} (a : zmod n) :
id └┘ └──┘ ┴
src └┘ └──┘
typ └┘ └──┘ ┴
doc └┘
354 (a.val : ℤ) = a.val_min_abs + if a.val ≤ n / 2 then 0 else n :=
id ┴└──┘ ┴ ┴ ┴└──────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ └──────────┘ ┴ └──┘ ┴ ┴
typ ┴└──┘ ┴ ┴ ┴└──────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────────┘
355 by simp [zmod.val_min_abs]; split_ifs; simp
id └──────────────┘
src └────┘└──────────────┘┴ └───────┘ └────
typ └────┘└──────────────┘┴ └───────┘ └────
doc └────┘└──────────────┘┴ └───────┘ └────
txt └────┘ ┴ └───────┘ └────
par └────┘ ┴ └───────┘ └────
pid ┴┴ ┴ └
st └─────────────────────────────────────────
356
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
357 lemma neg_eq_self_mod_two : ∀ (a : zmod 2), -a = a := dec_trivial
id └──┘ ┴┴ ┴ ┴ └─────────┘
src └──┘ ┴ ┴ └─────────┘
typ └──┘ ┴┴ ┴ ┴ └─────────┘
doc └─────────┘
358
359 @[simp] lemma nat_abs_mod_two (a : ℤ) : (a.nat_abs : zmod 2) = a :=
id ┴ ┴└──────┘ └──┘ ┴ ┴
src ┴ └──────┘ └──┘ ┴
typ ┴ ┴└──────┘ └──┘ ┴ ┴
doc └──┘
360 by cases a; simp [zmod.neg_eq_self_mod_two]
id ┴ └──────────────────────┘
src └────┘ └────┘└──────────────────────┘└─
typ └────┘┴ └────┘└──────────────────────┘└─
doc └────┘ └────┘ └─
txt └────┘ └────┘ └─
par └────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └─────────────────────────────────────────
361
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
362 section
363 variables {α : Type*} [has_zero α] [has_one α] [has_add α] {n : ℕ+}
id └──────┘ └─────┘ └─────┘ └┘
src └──────┘ └─────┘ └─────┘ └┘
typ └──────┘ └─────┘ └─────┘ └┘
doc └┘
364
365 def cast : zmod n → α := nat.cast ∘ fin.val
id └──┘ ┴ ┴ └──────┘ ┴ └─────┘
src └──┘ └──────┘ ┴ └─────┘
typ └──┘ ┴ ┴ └──────┘ ┴ └─────┘
doc └──────┘
366
367 end
368
369 end zmod
370
371 def zmodp (p : ℕ) (hp : prime p) : Type := zmod ⟨p, hp.pos⟩
id ┴ └───┘ ┴ └──┘ ┴ └┘└──┘
src ┴ └───┘ └──┘ └──┘
typ ┴ └───┘ ┴ └──┘ ┴ └┘└──┘
doc └───┘
372
373 namespace zmodp
374
375 variables {p : ℕ} (hp : prime p)
id ┴ └───┘
src ┴ └───┘
typ ┴ └───┘
doc └───┘
376
377 instance : comm_ring (zmodp p hp) := zmod.comm_ring ⟨p, hp.pos⟩
id └───────┘ └───┘ ┴ └┘ └────────────┘ ┴ └┘└──┘
src └───────┘ └───┘ └────────────┘ └──┘
typ └───────┘ └───┘ ┴ └┘ └────────────┘ ┴ └┘└──┘
378
379 instance : inhabited (zmodp p hp) := ⟨0⟩
id └───────┘ └───┘ ┴ └┘
src └───────┘ └───┘
typ └───────┘ └───┘ ┴ └┘
380
381 instance {p : ℕ} (hp : prime p) : has_inv (zmodp p hp) :=
id ┴ └───┘ ┴ └─────┘ └───┘ ┴ └┘
src ┴ └───┘ └─────┘ └───┘
typ ┴ └───┘ ┴ └─────┘ └───┘ ┴ └┘
doc └───┘
382 ⟨λ a, gcd_a a.1 p⟩
id ┴ └───┘ ┴┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴┴ ┴
doc └───┘
383
384 lemma add_val : ∀ a b : zmodp p hp, (a + b).val = (a.val + b.val) % p
id ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
src └───┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴
typ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
385 | ⟨_, _⟩ ⟨_, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
386
387 lemma mul_val : ∀ a b : zmodp p hp, (a * b).val = (a.val * b.val) % p
id ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
src └───┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴
typ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴
388 | ⟨_, _⟩ ⟨_, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
389
390 @[simp] lemma one_val : (1 : zmodp p hp).val = 1 :=
id └───┘ ┴ └┘ └─┘ ┴
src └───┘ └─┘ ┴
typ └───┘ ┴ └┘ └─┘ ┴
doc └──┘
391 nat.mod_eq_of_lt hp.one_lt
id └──────────────┘ └┘└─────┘
src └──────────────┘ └─────┘
typ └──────────────┘ └┘└─────┘
392
393 @[simp] lemma zero_val : (0 : zmodp p hp).val = 0 := rfl
id └───┘ ┴ └┘ └─┘ ┴ └─┘
src └───┘ └─┘ ┴ └─┘
typ └───┘ ┴ └┘ └─┘ ┴ └─┘
doc └──┘
394
395 lemma val_cast_nat (a : ℕ) : (a : zmodp p hp).val = a % p :=
id ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴
src ┴ └───┘ └─┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴
396 @zmod.val_cast_nat ⟨p, hp.pos⟩ _
id └───────────────┘ ┴ └┘└──┘
src └───────────────┘ └──┘
typ └───────────────┘ ┴ └┘└──┘
397
398 lemma mk_eq_cast {a : ℕ} (h : a < p) : (⟨a, h⟩ : zmodp p hp) = (a : zmodp p hp) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ └───┘ ┴ └┘
src ┴ ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ └───┘ ┴ └┘
399 @zmod.mk_eq_cast ⟨p, hp.pos⟩ _ _
id └─────────────┘ ┴ └┘└──┘
src └─────────────┘ └──┘
typ └─────────────┘ ┴ └┘└──┘
400
401 @[simp] lemma cast_self_eq_zero: (p : zmodp p hp) = 0 :=
id ┴ └───┘ ┴ └┘ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ └┘ ┴
doc └──┘
402 fin.eq_of_veq $ by simp [val_cast_nat]
id └───────────┘ └──────────┘
src └───────────┘ └────┘└──────────┘└─
typ └───────────┘ └────┘└──────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────
403
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
404 lemma val_cast_of_lt {a : ℕ} (h : a < p) : (a : zmodp p hp).val = a :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴
405 @zmod.val_cast_of_lt ⟨p, hp.pos⟩ _ h
id └─────────────────┘ ┴ └┘└──┘ ┴
src └─────────────────┘ └──┘
typ └─────────────────┘ ┴ └┘└──┘ ┴
406
407 @[simp] lemma cast_mod_nat (a : ℕ) : ((a % p : ℕ) : zmodp p hp) = a :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
doc └──┘
408 @zmod.cast_mod_nat ⟨p, hp.pos⟩ _
id └───────────────┘ ┴ └┘└──┘
src └───────────────┘ └──┘
typ └───────────────┘ ┴ └┘└──┘
409
410 @[simp] lemma cast_val (a : zmodp p hp) : (a.val : zmodp p hp) = a :=
id └───┘ ┴ └┘ ┴└──┘ └───┘ ┴ └┘ ┴ ┴
src └───┘ └──┘ └───┘ ┴
typ └───┘ ┴ └┘ ┴└──┘ └───┘ ┴ └┘ ┴ ┴
doc └──┘
411 @zmod.cast_val ⟨p, hp.pos⟩ _
id └───────────┘ ┴ └┘└──┘
src └───────────┘ └──┘
typ └───────────┘ ┴ └┘└──┘
412
413 @[simp] lemma cast_mod_int (a : ℤ) : ((a % p : ℤ) : zmodp p hp) = a :=
id ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴
doc └──┘
414 @zmod.cast_mod_int ⟨p, hp.pos⟩ _
id └───────────────┘ ┴ └┘└──┘
src └───────────────┘ └──┘
typ └───────────────┘ ┴ └┘└──┘
415
416 lemma val_cast_int (a : ℤ) : (a : zmodp p hp).val = (a % p).nat_abs :=
id ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └─────┘
src ┴ └───┘ └─┘ ┴ ┴ └─────┘
typ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └─────┘
417 @zmod.val_cast_int ⟨p, hp.pos⟩ _
id └───────────────┘ ┴ └┘└──┘
src └───────────────┘ └──┘
typ └───────────────┘ ┴ └┘└──┘
418
419 lemma coe_val_cast_int (a : ℤ) : ((a : zmodp p hp).val : ℤ) = a % (p : ℕ) :=
id ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
420 @zmod.coe_val_cast_int ⟨p, hp.pos⟩ _
id └───────────────────┘ ┴ └┘└──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ ┴ └┘└──┘
421
422 lemma eq_iff_modeq_nat {a b : ℕ} : (a : zmodp p hp) = b ↔ a ≡ b [MOD p] :=
id ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴
doc ┴ └──┘ ┴
423 @zmod.eq_iff_modeq_nat ⟨p, hp.pos⟩ _ _
id └───────────────────┘ ┴ └┘└──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ ┴ └┘└──┘
424
425 lemma eq_iff_modeq_int {a b : ℤ} : (a : zmodp p hp) = b ↔ a ≡ b [ZMOD p] :=
id ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴┴
src ┴ └───┘ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴┴
426 @zmod.eq_iff_modeq_int ⟨p, hp.pos⟩ _ _
id └───────────────────┘ ┴ └┘└──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ ┴ └┘└──┘
427
428 lemma eq_zero_iff_dvd_nat (a : ℕ) : (a : zmodp p hp) = 0 ↔ p ∣ a :=
id ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
429 @zmod.eq_zero_iff_dvd_nat ⟨p, hp.pos⟩ _
id └──────────────────────┘ ┴ └┘└──┘
src └──────────────────────┘ └──┘
typ └──────────────────────┘ ┴ └┘└──┘
430
431 lemma eq_zero_iff_dvd_int (a : ℤ) : (a : zmodp p hp) = 0 ↔ (p : ℤ) ∣ a :=
id ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
432 @zmod.eq_zero_iff_dvd_int ⟨p, hp.pos⟩ _
id └──────────────────────┘ ┴ └┘└──┘
src └──────────────────────┘ └──┘
typ └──────────────────────┘ ┴ └┘└──┘
433
434 instance : fintype (zmodp p hp) := @zmod.fintype ⟨p, hp.pos⟩
id └─────┘ └───┘ ┴ └┘ └──────────┘ ┴ └┘└──┘
src └─────┘ └───┘ └──────────┘ └──┘
typ └─────┘ └───┘ ┴ └┘ └──────────┘ ┴ └┘└──┘
doc └─────┘
435
436 instance decidable_eq : decidable_eq (zmodp p hp) := fin.decidable_eq _
id └──────────┘ └───┘ ┴ └┘ └──────────────┘
src └──────────┘ └───┘ └──────────────┘
typ └──────────┘ └───┘ ┴ └┘ └──────────────┘
437
438 instance : has_repr (zmodp p hp) := fin.has_repr _
id └──────┘ └───┘ ┴ └┘ └──────────┘
src └──────┘ └───┘ └──────────┘
typ └──────┘ └───┘ ┴ └┘ └──────────┘
439
440 @[simp] lemma card_zmodp : fintype.card (zmodp p hp) = p :=
id └──────────┘ └───┘ ┴ └┘ ┴ ┴
src └──────────┘ └───┘ ┴
typ └──────────┘ └───┘ ┴ └┘ ┴ ┴
doc └──┘ └──────────┘
441 @zmod.card_zmod ⟨p, hp.pos⟩
id └────────────┘ ┴ └┘└──┘
src └────────────┘ └──┘
typ └────────────┘ ┴ └┘└──┘
442
443 lemma le_div_two_iff_lt_neg {p : ℕ} (hp : prime p) (hp1 : p % 2 = 1)
id ┴ └───┘ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘
444 {x : zmodp p hp} (hx0 : x ≠ 0) : x.1 ≤ (p / 2 : ℕ) ↔ (p / 2 : ℕ) < (-x).1 :=
id └───┘ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
445 @zmod.le_div_two_iff_lt_neg ⟨p, hp.pos⟩ hp1 _ hx0
id └────────────────────────┘ ┴ └┘└──┘ └─┘ └─┘
src └────────────────────────┘ └──┘
typ └────────────────────────┘ ┴ └┘└──┘ └─┘ └─┘
446
447 lemma ne_neg_self (hp1 : p % 2 = 1) {a : zmodp p hp} (ha : a ≠ 0) : a ≠ -a :=
id ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴
448 @zmod.ne_neg_self ⟨p, hp.pos⟩ hp1 _ ha
id └──────────────┘ ┴ └┘└──┘ └─┘ └┘
src └──────────────┘ └──┘
typ └──────────────┘ ┴ └┘└──┘ └─┘ └┘
449
450 variable {hp}
451
452 /-- `val_min_abs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
453 The result will be in the interval `(-n/2, n/2]` -/
454 def val_min_abs (x : zmodp p hp) : ℤ := zmod.val_min_abs x
id └───┘ ┴ └┘ ┴ └──────────────┘ ┴
src └───┘ ┴ └──────────────┘
typ └───┘ ┴ └┘ ┴ └──────────────┘ ┴
doc └──────────────┘
455
456 @[simp] lemma coe_val_min_abs (x : zmodp p hp) :
id └───┘ ┴ └┘
src └───┘
typ └───┘ ┴ └┘
doc └──┘
457 (x.val_min_abs : zmodp p hp) = x :=
id ┴└──────────┘ └───┘ ┴ └┘ ┴ ┴
src └──────────┘ └───┘ ┴
typ ┴└──────────┘ └───┘ ┴ └┘ ┴ ┴
doc └──────────┘
458 zmod.coe_val_min_abs x
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
459
460 lemma nat_abs_val_min_abs_le (x : zmodp p hp) : x.val_min_abs.nat_abs ≤ p / 2 :=
id └───┘ ┴ └┘ ┴└──────────┘└──────┘ ┴ ┴ ┴
src └───┘ └──────────┘└──────┘ ┴ ┴
typ └───┘ ┴ └┘ ┴└──────────┘└──────┘ ┴ ┴ ┴
doc └──────────┘
461 zmod.nat_abs_val_min_abs_le x
id └─────────────────────────┘ ┴
src └─────────────────────────┘
typ └─────────────────────────┘ ┴
462
463 @[simp] lemma val_min_abs_zero : (0 : zmodp p hp).val_min_abs = 0 :=
id └───┘ ┴ └┘ └─────────┘ ┴
src └───┘ └─────────┘ ┴
typ └───┘ ┴ └┘ └─────────┘ ┴
doc └──┘ └─────────┘
464 zmod.val_min_abs_zero
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
465
466 @[simp] lemma val_min_abs_eq_zero (x : zmodp p hp) : x.val_min_abs = 0 ↔ x = 0 :=
id └───┘ ┴ └┘ ┴└──────────┘ ┴ ┴ ┴ ┴
src └───┘ └──────────┘ ┴ ┴ ┴
typ └───┘ ┴ └┘ ┴└──────────┘ ┴ ┴ ┴ ┴
doc └──┘ └──────────┘
467 zmod.val_min_abs_eq_zero x
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
468
469 lemma cast_nat_abs_val_min_abs (a : zmodp p hp) :
id └───┘ ┴ └┘
src └───┘
typ └───┘ ┴ └┘
470 (a.val_min_abs.nat_abs : zmodp p hp) = if a.val ≤ p / 2 then a else -a :=
id ┴└──────────┘└──────┘ └───┘ ┴ └┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴┴
src └──────────┘└──────┘ └───┘ ┴ └──┘ ┴ ┴ ┴
typ ┴└──────────┘└──────┘ └───┘ ┴ └┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴┴
doc └──────────┘
471 zmod.cast_nat_abs_val_min_abs a
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
472
473 @[simp] lemma nat_abs_val_min_abs_neg (a : zmodp p hp) :
id └───┘ ┴ └┘
src └───┘
typ └───┘ ┴ └┘
doc └──┘
474 (-a).val_min_abs.nat_abs = a.val_min_abs.nat_abs :=
id ┴┴ └─────────┘ └─────┘ ┴ ┴└──────────┘└──────┘
src ┴ └─────────┘ └─────┘ ┴ └──────────┘└──────┘
typ ┴┴ └─────────┘ └─────┘ ┴ ┴└──────────┘└──────┘
doc └─────────┘ └──────────┘
475 zmod.nat_abs_val_min_abs_neg _
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
476
477 lemma val_eq_ite_val_min_abs (a : zmodp p hp) :
id └───┘ ┴ └┘
src └───┘
typ └───┘ ┴ └┘
478 (a.val : ℤ) = a.val_min_abs + if a.val ≤ p / 2 then 0 else p :=
id ┴└──┘ ┴ ┴ ┴└──────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ └──────────┘ ┴ └──┘ ┴ ┴
typ ┴└──┘ ┴ ┴ ┴└──────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────────┘
479 zmod.val_eq_ite_val_min_abs _
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
480
481 variable (hp)
482
483 lemma prime_ne_zero {q : ℕ} (hq : prime q) (hpq : p ≠ q) : (q : zmodp p hp) ≠ 0 :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
src ┴ └───┘ ┴ └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ ┴
doc └───┘
484 by rwa [← nat.cast_zero, ne.def, zmodp.eq_iff_modeq_nat, nat.modeq.modeq_zero_iff,
id └───────────┘ └────┘ └────────────────────┘ └──────────────────────┘
src └─────┘└───────────┘└┘└────┘└┘└────────────────────┘└┘└──────────────────────┘└─
typ └─────┘└───────────┘└┘└────┘└┘└────────────────────┘└┘└──────────────────────┘└─
doc └─────┘ └┘ └┘ └┘ └─
txt └─────┘ └┘ └┘ └┘ └─
par └─────┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ └─
st └───────────────────┘└──────┘└──────────────────────┘└────────────────────────┘└─
485 ← hp.coprime_iff_not_dvd, coprime_primes hp hq]
id └────────────┘ └┘ └┘
src ───┘ └┘└────────────┘┴ ┴ └─
typ ───┘└────────────────────┘└┘└────────────┘┴└┘┴└┘└─
doc ───┘ └┘ ┴ ┴ └─
txt ───┘ └┘ ┴ ┴ └─
par ───┘ └┘ ┴ ┴ └─
pid ───┘ └┘ ┴ ┴ ┴└
st ─────────────────────────┘└────────────────────┘┴└
486
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
487 lemma mul_inv_eq_gcd (a : ℕ) : (a : zmodp p hp) * a⁻¹ = nat.gcd a p :=
id ┴ ┴ └───┘ ┴ └┘ ┴ ┴└┘ ┴ └─────┘ ┴ ┴
src ┴ └───┘ ┴ └┘ ┴ └─────┘
typ ┴ ┴ └───┘ ┴ └┘ ┴ ┴└┘ ┴ └─────┘ ┴ ┴
488 by rw [← int.cast_coe_nat (nat.gcd _ _), nat.gcd_comm, nat.gcd_rec, ← (eq_iff_modeq_int _).2 (int.modeq.gcd_a_modeq _ _)];
id └──────────────┘ └─────┘ └──────────┘ └─────────┘ └──────────────┘ └───────────────────┘
src └────┘└──────────────┘┴ └─────┘└─────┘└──────────┘└┘└─────────┘└──┘ └──────────────┘└────┘ └───────────────────┘└────┘
typ └────┘└──────────────┘┴ └─────┘└─────┘└──────────┘└┘└─────────┘└──┘ └──────────────┘└────┘ └───────────────────┘└────┘
doc └────┘ ┴ └─────┘ └┘ └──┘ └────┘ └────┘
txt └────┘ ┴ └─────┘ └┘ └──┘ └────┘ └────┘
par └────┘ ┴ └─────┘ └┘ └──┘ └────┘ └────┘
pid └──┘ ┴ └─────┘ └┘ └──┘ └────┘ └────┘
st └───────────────────────────────────┘└────────────┘└───────────┘└────────────────────────────────────────────────────┘┴└─
489 simp [has_inv.inv, val_cast_nat]
id └──────────┘
src └────┘ └┘└──────────┘└─
typ └────┘ └┘└──────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ───────────────────────────────────
490
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
491 private lemma mul_inv_cancel_aux : ∀ a : zmodp p hp, a ≠ 0 → a * a⁻¹ = 1 :=
id └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴└┘ ┴
src └───┘ ┴ ┴ └┘ ┴
typ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴└┘ ┴
492 λ ⟨a, hap⟩ ha0, begin
id ┴ └─┘
typ ┴ └─┘
st └─────
493 rw [mk_eq_cast, ne.def, ← @nat.cast_zero (zmodp p hp), eq_iff_modeq_nat, modeq_zero_iff] at ha0,
id └────────┘ └────┘ └───────────┘ └───┘ ┴ └┘ └──────────────┘ └────────────┘
src └──┘└────────┘└┘└────┘└──┘ └───────────┘┴ └───┘┴ ┴ └─┘└──────────────┘└┘└────────────┘└──────┘
typ └──┘└────────┘└┘└────┘└──┘ └───────────┘┴ └───┘┴┴┴└┘└─┘└──────────────┘└┘└────────────┘└──────┘
doc └──┘ └┘ └──┘ ┴ ┴ ┴ └─┘ └┘ └──────┘
txt └──┘ └┘ └──┘ ┴ ┴ ┴ └─┘ └┘ └──────┘
par └──┘ └┘ └──┘ ┴ ┴ ┴ └─┘ └┘ └──────┘
pid └┘ └┘ └──┘ ┴ ┴ ┴ └─┘ └┘ ┴└─────┘
st ───────────────┘└──────┘└─────────────────────────────┘└────────────────┘└──────────────┘┴└─────┘└─
494 have : nat.gcd p a = 1 := (prime.coprime_iff_not_dvd hp).2 ha0,
id └─────┘ ┴ ┴ ┴ └───────────────────────┘ └┘ └─┘
src └─────┘└─────┘┴ ┴ ┴┴└────┘ └───────────────────────┘┴ └──┘
typ └─────┘└─────┘┴┴┴┴┴┴└────┘ └───────────────────────┘┴└┘└──┘└─┘
doc └─────┘ ┴ ┴ ┴ └────┘ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └────┘ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └────┘ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴└───┘ ┴ └──┘
st ───────────────────────────────────────────────────────────────┘└─
495 rw [mk_eq_cast _ hap, mul_inv_eq_gcd, nat.gcd_comm],
id └────────┘ └─┘ └────────────┘ └──────────┘
src └──┘└────────┘└─┘ └┘└────────────┘└┘└──────────┘┴
typ └──┘└────────┘└─┘└─┘└┘└────────────┘└┘└──────────┘┴
doc └──┘ └─┘ └┘ └┘ ┴
txt └──┘ └─┘ └┘ └┘ ┴
par └──┘ └─┘ └┘ └┘ ┴
pid └┘ └─┘ └┘ └┘ ┴
st ─────────────────────┘└──────────────┘└────────────┘└──
496 simpa [nat.gcd_comm, this]
id └──────────┘ └──┘
src └─────┘└──────────┘└┘ └┘
typ └─────┘└──────────┘└┘└──┘└┘
doc └─────┘ └┘ └┘
txt └─────┘ └┘ └┘
par └─────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ────────────────────────────┘
497 end
st └─┘
498
499 instance : discrete_field (zmodp p hp) :=
id └────────────┘ └───┘ ┴ └┘
src └────────────┘ └───┘
typ └────────────┘ └───┘ ┴ └┘
500 { zero_ne_one := fin.ne_of_vne $ show 0 ≠ 1 % p,
id └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴
501 by rw nat.mod_eq_of_lt hp.one_lt;
id └──────────────┘ └───────┘
src └─┘└──────────────┘┴└───────┘
typ └─┘└──────────────┘┴└───────┘
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └───────────────────────────────
502 exact zero_ne_one,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘
503 mul_inv_cancel := mul_inv_cancel_aux hp,
id └────────────────┘ └┘
src └────────────────┘
typ └────────────────┘ └┘
504 inv_mul_cancel := λ a, by rw mul_comm; exact mul_inv_cancel_aux hp _,
id ┴ └──────┘ └────────────────┘ └┘
src └─┘└──────┘ └────┘└────────────────┘┴ └┘
typ ┴ └─┘└──────┘ └────┘└────────────────┘┴└┘└┘
doc └─┘ └────┘ ┴ └┘
txt └─┘ └────┘ ┴ └┘
par └─┘ └────┘ ┴ └┘
pid ┴ ┴ ┴ └┘
st └─────────────────────────────────────────┘
505 has_decidable_eq := by apply_instance,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
506 inv_zero := show (gcd_a 0 p : zmodp p hp) = 0,
id └───┘ ┴ └───┘ ┴ └┘ ┴
src └───┘ └───┘ ┴
typ └───┘ ┴ └───┘ ┴ └┘ ┴
doc └───┘
507 by unfold gcd_a xgcd xgcd_aux; refl,
src └────────────────────────┘ └──┘
typ └────────────────────────┘ └──┘
doc └────────────────────────┘ └──┘
txt └────────────────────────┘ └──┘
par └────────────────────────┘ └──┘
pid └──────────────────┘
st └───────────────────────────────┘
508 ..zmodp.comm_ring hp,
id └─────────────┘ └┘
src └─────────────┘
typ └─────────────┘ └┘
509 ..zmodp.has_inv hp }
id └───────────┘ └┘
src └───────────┘
typ └───────────┘ └┘
510
511 end zmodp